Commit 70a8c43d authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/andre/enable-warning-6' into 'master'

synchronize with !3631

See merge request frama-c/meta!58
parents 537081e3 4b996570
......@@ -119,7 +119,7 @@ let add_ghost_code flags =
let base_type = Logic_utils.logicCType typ in
(* The _set is either a fixed array or a pointer *)
let ctype = match flags.static_bindings with
| Some n -> TArray (base_type, Some (Cil.integer unkloc n), [])
| Some n -> TArray (base_type, Some (Cil.integer ~loc:unkloc n), [])
| None -> TPtr (base_type, [])
in
let var = Cil.makeGlobalVar (setname name) ctype in
......@@ -194,8 +194,8 @@ let make_dynamic_modif_code name lvar =
let sizevar = search_global_var (sizename name) in
let capvar = search_global_var (capname name) in
List.rev [
(let cond = Cil.mkBinOp unkloc Gt (Cil.evar sizevar) (Cil.evar capvar) in
let newsize = Cil.mkBinOp unkloc Mult (Cil.integer unkloc 2)
(let cond = Cil.mkBinOp ~loc:unkloc Gt (Cil.evar sizevar) (Cil.evar capvar) in
let newsize = Cil.mkBinOp ~loc:unkloc Mult (Cil.integer ~loc:unkloc 2)
(Cil.increm (Cil.evar sizevar) 1) in
let realloc = Globals.Functions.find_by_name "realloc" |>
Kernel_function.get_vi |> Cil.evar in
......@@ -203,8 +203,8 @@ let make_dynamic_modif_code name lvar =
let incinstr = Call (None, realloc, [arg; newsize], unkloc) in
let inc = Cil.mkStmtOneInstr ~ghost:true incinstr in
Cil.mkStmt ~ghost:true (If (cond, Cil.mkBlock [inc], Cil.mkBlock [], unkloc)));
(let addr = Cil.mkBinOp unkloc PlusPI (Cil.evar tabvar) (Cil.evar sizevar) in
let tabcell = Cil.mkMem addr NoOffset in
(let addr = Cil.mkBinOp ~loc:unkloc PlusPI (Cil.evar tabvar) (Cil.evar sizevar) in
let tabcell = Cil.mkMem ~addr ~off:NoOffset in
let value = Option.get lvar.lv_origin |> Cil.evar in
Cil.mkStmtOneInstr ~ghost:true (Set (tabcell, value, unkloc)));
(let increxp = Cil.increm (Cil.evar sizevar) 1 in
......
......@@ -386,14 +386,14 @@ go :- %a
| None ->
(* This happens if Prolog get stuck and is not interruptible, for an obuscure reaons *)
Self.warning "%s : PROLOG FAILURE, (%d ATTEMPTS)" mp.mp_name max_attempts;
Property_status.emit emitter [] ip Property_status.False_and_reachable;
Property_status.emit emitter ~hyps:[] ip Property_status.False_and_reachable;
false
| Some 0 -> (* Property could be deduced, propagate status *)
Self.feedback "%s : OK" mp.mp_name;
Property_status.emit emitter [] ip Property_status.True; true
Property_status.emit emitter ~hyps:[] ip Property_status.True; true
| Some _ -> (* Property could not be deduced, propagate FALSE to be safe *)
Self.warning "%s : FAILURE" mp.mp_name;
Property_status.emit emitter [] ip Property_status.False_and_reachable;
Property_status.emit emitter ~hyps:[] ip Property_status.False_and_reachable;
false
in
Sys.chdir current_dir;
......
......@@ -153,11 +153,11 @@ let finalize_dependencies () =
(* If the MP is admitted, every instance *is* true *)
if prop.ump_admit then
List.iter (fun inst ->
Property_status.emit prop.ump_emitter [] inst Property_status.True
Property_status.emit prop.ump_emitter ~hyps:[] inst Property_status.True
) deps
else (
(* The MP is true if every instance is true *)
Property_status.emit prop.ump_emitter deps prop.ump_ip Property_status.True
Property_status.emit prop.ump_emitter ~hyps:deps prop.ump_ip Property_status.True
)
in
Seq.iter add_one keys
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment