Frama-C: Die Werte der Aussage

Question

Ich möchte ein Frama-C-Plugin entwickeln, wo ich die Werte der aktuellen Aussage bekomme.

Mit Hilfe dieses Beitrags Frama-C Plugin development: Getting result of value-analysis war ich in der Lage, die Werte der Anweisungen zu drucken, aber Pointer wurden nicht so gezeigt, wie ich es brauche.

Mit Hilfe der Kommentare konnte ich den gesamten Zustand (nicht nur die Variablen der Anweisung) drucken.

Kann ich diese beiden kombinieren: Get die Variablen der Anweisung, aber auch mit den Dereferenzierten Zeigern (der Wert)?

Zum Beispiel das Drucken eines Nicht-Zeiger nach Aussage x=1 Ergebnisse in x -> {{ NULL -> {1} }}, während ein Zeiger Druck nach einer Anweisung wie * x = 3, ergibt x -> {{ y -> {0} }}, weil die 0 die der variablen versetzt ist, aber ich möchte Holen Sie sich den Wert, auf den der Zeiger zeigt, im Beispiel 3. So wie ich es möchte, wäre etwas so zu bekommen: x -> 3.

Noch besser wäre es, ein Tupel von (String varname, int value) zu bekommen, damit ich es selbst ausdrucken kann.

Answer 1

Der Wert einer Variablen hängt von ihrem Typ ab. Wenn also die Variable den Typ int hat, ist ihr Wert eine Ganzzahl, aber wenn die Variable den Typ int* hat, ist ihr Wert die Adresse einer int Variablen. Die Variable kann viele andere Typen wie Struktur, Array usw. haben.

Von Ihrem Beispiel scheint es, dass Sie den Wert der Variablen vom Zeiger angezeigt bekommen möchten. Beachten Sie, dass in einigen Fällen ist dies keine gültige Operation ...

Wie dem auch sei, nehme ich an, dass Sie diese Funktion extrahieren kann in Frama-C Plugin development: Getting result of value-analysis einen L-Wert aus der vorherigen Antwort drucken:

let pretty_lval fmt stmt lval = 
    let kinstr = Kstmt stmt in (* make a kinstr from a stmt *) 
    let loc = (* make a location from a kinstr + an lval *) 
    !Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval 
    in 
    Db.Value.fold_state_callstack 
    (fun state() -> 
     (* for each state in the callstack *) 
     let value = Db.Value.find state loc in (* obtain value for location *) 
     Format.fprintf fmt "%a -> %a@." Printer.pp_lval lval 
     Locations.Location_Bytes.pretty value (* print mapping *) 
    )() ~after:false kinstr 

Sie können dann Drucken Sie die Informationen, die Sie suchen mit:

if Cil.isPointerType vi.vtype then 
    let lval = (Mem (Cil.evar vi), NoOffset) in 
    pretty_lval fmt stmt lval