Commit 5ceb9812 authored by Julien Signoles's avatar Julien Signoles
Browse files

hack for fixing issue with fopen

parent 13a5e905
......@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
-* E-ACSL [2015/04/28] Fix bug when using fopen.
o E-ACSL [2014/12/17] Export a minimal API for other plug-ins.
-* E-ACSL [2014/10/27] Add a missing cast when translating an integral
type used in a floating point/real context in an annotation.
......
......@@ -219,11 +219,12 @@ let change_printer =
class printer = object
inherit X.printer as super
method !varinfo fmt vi =
if not vi.Cil_types.vghost then
if vi.Cil_types.vghost || vi.Cil_types.vstorage <> Cil_types.Extern
then
super#varinfo fmt vi
else
let s = Str.replace_first r "" vi.Cil_types.vname in
Format.fprintf fmt "%s" s
else
super#varinfo fmt vi
end
end in
Printer.update_printer (module Printer_class: Printer.PrinterExtension)
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,15 +4,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &fopen[0] }}
__fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
......
......@@ -4,15 +4,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &fopen[0] }}
__fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
......
......@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
......
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
random_counter ∈ {0}
rand_max ∈ {32767}
__fc_random_counter ∈ {0}
__fc_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