Skip to content
Snippets Groups Projects
Commit afae5600 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[Instantiate] Lint

parent d9ca6cfe
No related branches found
No related tags found
No related merge requests found
......@@ -87,4 +87,4 @@ let globals loc =
let axiomatic name list loc = annot(Daxiomatic(name, list, [], loc)) loc in
let l = Table.fold (fun _ x l -> fun_or_pred x loc :: l) logic_functions l in
let l = Table.fold (fun n x l -> axiomatic n x loc :: l) axiomatics l in
l
\ No newline at end of file
l
......@@ -54,9 +54,9 @@ val get_logic_function: string -> (unit -> logic_info) -> logic_info
Note that function overloading is not supported.
*)
val get_logic_function_in_axiomatic:
string ->
(unit -> (string * global_annotation list) * logic_info list) ->
logic_info
string ->
(unit -> (string * global_annotation list) * logic_info list) ->
logic_info
(** Clears internal tables *)
val clear: unit -> unit
......
......@@ -76,7 +76,7 @@ let make_axiomatic_is_allocable loc () =
let max =
tinteger
(Integer.to_int
(Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
(Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
in
let label = FormalLabel("L") in
let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment