diff --git a/src/plugins/instantiate/global_context.ml b/src/plugins/instantiate/global_context.ml index 9a6d4ff32d6ff6cf6e9e7c9b37db0e9bfb726fc7..9791a78d529581153916776dd28b906b02c35232 100644 --- a/src/plugins/instantiate/global_context.ml +++ b/src/plugins/instantiate/global_context.ml @@ -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 diff --git a/src/plugins/instantiate/global_context.mli b/src/plugins/instantiate/global_context.mli index 89f3a2124493da562f1fb01dd8e955b37b3f1f6a..9a1456ff0bb26db8834f8857a883749d52e91b8b 100644 --- a/src/plugins/instantiate/global_context.mli +++ b/src/plugins/instantiate/global_context.mli @@ -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 diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml index 3f9ced7c231c90ccc69f6782abddb0d012d47790..a35a97b53e37d96e97149e0bb851c4db758cac6c 100644 --- a/src/plugins/instantiate/stdlib/basic_alloc.ml +++ b/src/plugins/instantiate/stdlib/basic_alloc.ml @@ -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