Commit bc153f5c authored by Julien Signoles's avatar Julien Signoles
Browse files

fix bug when using Frama-C-specific names of the libc which prevent linking the generated code

parent 3384b7f8
......@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
-* E-ACSL [2014/07/08] Fix bug about using some part of the
(Frama-C) libc which prevents linking of the generated C code.
-* E-ACSL [2014/05/21] Fix bug #1782 about incorrect URL in the
documentation.
- E-ACSL [2014/03/27] Remove spurious warnings when using type `real`.
......
......@@ -197,10 +197,39 @@ let add_e_acsl_library _files =
- locations are better (indicate an existing file, and not a temp file) *)
let () = Cmdline.run_after_configuring_stage add_e_acsl_library
(* The Frama-C standard library contains specific built-in variables prefixed by
"__fc_" and declared as extern: they prevent the generated code to be
linked. This modification of the default printer replaces them by their
original version from the stdlib. For instance, [__fc_stdout] is replaced by
[stdout]. That is very hackish since it modifies the default Frama-C
printer.
TODO: should be done by the Frama-C default printer at some points. *)
let change_printer =
(* not projectified on purpose: this printer change is common to each
project. *)
let first = ref true in
fun () ->
if !first then begin
first := false;
let r = Str.regexp "^__fc_" in
let pp () = object
inherit (Printer.extensible_printer ()) as super
method !varinfo fmt vi =
if not vi.Cil_types.vghost then
let s = Str.replace_first r "" vi.Cil_types.vname in
Format.fprintf fmt "%s" s
else
super#varinfo fmt vi
end in
Printer.change_printer pp
end
let main () =
if Options.Run.get () then
if Options.Run.get () then begin
change_printer ();
ignore (generate_code (Options.Project_name.get ()))
else
end else
if Options.Check.get () then
apply_on_e_acsl_ast
(fun () ->
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -14,8 +14,8 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -14,8 +14,8 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
Markdown is supported
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