Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692020-06-02T15:51:12ZOpen-Source Projects
Redmine Deductive Verification Tools for Linux Kernel - Bug #10364 (New): Ubuntu19: ERROR while compiling...https://forge.ispras.ru/issues/103642020-06-02T15:51:12ZDenis Efremovefremov@ispras.ru
<p>System: Ubuntu 19</p>
<p>Error:<br /><pre>
#=== ERROR while compiling astraver-translator.v20.0 ==========================#
# context 2.0.4 | linux/x86_64 | ocaml-base-compiler.4.10.0 | git+https://forge.ispras.ru/git/astraver.opam-repository.git
# path ~/.opam/4.10.0/.opam-switch/build/astraver-translator.v20.0
# command ~/.opam/4.10.0/.opam-switch/build/astraver-translator.v20.0/./touch.sh
# exit-code 127
# env-file ~/.opam/log/astraver-translator-21105-60459a.env
# output-file ~/.opam/log/astraver-translator-21105-60459a.out
</pre></p>
<p>Steps to reproduce:<br /><pre>
$ sudo apt install opam
$ opam init -c 4.10.0 --disable-sandboxing
$ eval $(opam env)
$ opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
$ opam update
$ opam install depext
$ opam depext --install astraver
</pre></p>
<p>Workaround: don't use --disable-sandboxing during installation.</p> Deductive Verification Tools for Linux Kernel - Feature #10361 (New): Static initialization of fl...https://forge.ispras.ru/issues/103612020-05-29T14:10:54ZEvgeny Novikovnovikov@ispras.ru
<p>There are quite many failures related with this unsupported feature during verification of Linux loadable kernel modules. If this is not hard to implement this feature, it would be great.</p>
<p>A attached an example of the C source file for which there are following errors:<br /><pre>
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:18:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:119:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:175:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:231:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:287:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:343:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:398:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:454:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:510:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] /home/debian/klever-inst/klever/build bases/linux-5.5/Storage/home/zakharov/src/linux-stable/drivers/media/i2c/et8ek8/et8ek8_mode.c:565:0: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] User Error: skipping file /home/debian/klever-inst/klever-work/native-scheduler/scheduler/jobs/9e762226-2206-4f95-9b31-3095b99785e8/klever-core-work-dir/job/vtg/drivers/media/i2c/et8ek8/et8ek8.ko/memory safety/weaver/et8ek8_mode.c that has errors.
[kernel] Frama-C aborted: invalid user input.
</pre></p> Deductive Verification Tools for Linux Kernel - Bug #10027 (New): jc: typing error: Unsupported ...https://forge.ispras.ru/issues/100272020-01-09T22:45:31ZDenis Efremovefremov@ispras.ru
<pre>
$ frama-c -av nlist_init.c
[kernel] Parsing nlist_init.c (with preprocessing)
In file included from nlist_init.c:1:
nlist.h:6: warning: "NULL" redefined
6 | #define NULL ((void*) 0)
|
In file included from /home/work/.opam/astraver/share/frama-c/astraver/astraver_spec_prolog.h:33,
from <command-line>:
/usr/lib/gcc/x86_64-linux-gnu/9/include/stddef.h:395: note: this is the location of the previous definition
395 | #define NULL ((void *)0)
|
/home/work/.opam/astraver/share/frama-c/astraver/astraver_spec_prolog.h:131: warning: "NULL" redefined
/tmp/ppannot718bab.c:390: note: this is the location of the previous definition
390 | #define NULL ((void *)0)
|
[av] Starting AstraVer translation
[av] Warning: \separated is not supported by AstraVer. This predicate will be ignored
[av] Producing files for AstraVer in subdir nlist_init.c.av
[av] File nlist_init.c.av/nlist_init_c.jc written.
[av] File nlist_init.c.av/nlist_init_c.cloc written.
[av] Calling AstraVer tool in subdir nlist_init.c.av
FIXME: Warning: ignoring second declaration of function linked_n_starting_from_null_empty
FIXME: Warning: ignoring second declaration of function linked_n_all_elements_valid
FIXME: Warning: ignoring second declaration of function linked_n_first_valid
FIXME: Warning: ignoring second declaration of function linked_n_bounds
FIXME: Warning: ignoring second declaration of function linked_n_valid_range
FIXME: Warning: ignoring second declaration of function linked_n_next_of_all_indexes
FIXME: Warning: ignoring second declaration of function linked_n_before_last
FIXME: Warning: ignoring second declaration of function linked_n_split_segment
FIXME: Warning: ignoring second declaration of function linked_n_split_segment_direct
FIXME: Warning: ignoring second declaration of function linked_n_split_segment_right
FIXME: Warning: ignoring second declaration of function linked_n_split_segment_right_direct
FIXME: Warning: ignoring second declaration of function linked_n_merge_segment
FIXME: Warning: ignoring second declaration of function linked_n_merge_segment_right
FIXME: Warning: ignoring second declaration of function linked_n_all_elements
FIXME: Warning: ignoring second declaration of function index_of_not_in_subrange
FIXME: Warning: ignoring second declaration of function index_of_unexisting_item
FIXME: Warning: ignoring second declaration of function index_of_up_unexisting_item
FIXME: Warning: ignoring second declaration of function index_of_inter_existing_item
FIXME: Warning: ignoring second declaration of function index_of
FIXME: Warning: ignoring second declaration of function index_of_bounds_weak
FIXME: Warning: ignoring second declaration of function index_of_existing_item_weak
File "nlist_init_c.jc", line 694, characters 44-283: typing error: Unsupported range in term, sorry
[av] User Error: AstraVer subprocess failed: astraver -v -locs nlist_init_c.cloc nlist_init_c.jc
[kernel] Plug-in av aborted: invalid user input.
</pre> Deductive Verification Tools for Linux Kernel - Bug #10026 (New): postaction_term: unexpected ter...https://forge.ispras.ru/issues/100262020-01-09T18:10:36ZDenis Efremovefremov@ispras.ru
<pre>
$ frama-c -av hlist_add_head.c
[kernel] Parsing result/hlist_add_head.c (with preprocessing)
[av] Starting AstraVer translation
[av] Warning: \separated is not supported by AstraVer. This predicate will be ignored
[av] result/hlist_add_head.c:24:32: Failure:
postaction_term: unexpected term: &v_n_1
[kernel] Current source was: result/hlist_add_head.c:24
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 533, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1099, characters 17-55
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 526, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 529, characters 9-16
Called from file "common.ml", line 1959, characters 22-25
Called from file "common.ml" (inlined), line 2154, characters 42-45
Called from file "common.ml", line 2164, characters 77-83
Called from file "src/kernel_services/ast_queries/cil.ml", line 2370, characters 12-63
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 2774, characters 17-35
Called from file "src/kernel_services/ast_queries/cil.ml", line 2786, characters 12-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 2768, characters 17-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 2772, characters 17-40
Called from file "src/kernel_services/ast_queries/cil.ml", line 2821, characters 12-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 2768, characters 17-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 2763, characters 11-34
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/visitors/visitor.ml", line 196, characters 22-53
Called from file "list.ml", line 117, characters 24-34
Called from file "src/kernel_services/ast_data/annotations.ml", line 631, characters 8-27
Called from file "hashtbl.ml", line 317, characters 23-40
Called from file "hashtbl.ml", line 324, characters 14-35
Re-raised at file "hashtbl.ml", line 330, characters 4-13
Called from file "src/kernel_services/ast_data/annotations.ml", line 635, characters 4-57
Called from file "src/kernel_services/visitors/visitor.ml", line 211, characters 10-67
Called from file "src/kernel_services/visitors/visitor.ml", line 228, characters 8-253
Called from file "src/kernel_services/visitors/visitor.ml", line 423, characters 21-41
Called from file "list.ml", line 99, characters 22-25
Called from file "src/kernel_services/visitors/visitor.ml", line 421, characters 8-398
Called from file "src/kernel_services/visitors/visitor.ml", line 623, characters 38-54
Called from file "src/kernel_services/visitors/visitor.ml", line 815, characters 6-21
Called from file "src/kernel_services/ast_queries/cil.ml", line 3865, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6623, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6628, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6630, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6647, characters 15-39
Called from file "rewrite.ml", line 2505, characters 2-8
Called from file "norm.ml" (inlined), line 2056, characters 14-33
Called from file "norm.ml", line 2072, characters 2-83
Called from file "register.ml", line 153, characters 2-21
Called from file "register.ml", line 303, characters 6-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
</pre> Deductive Verification Tools for Linux Kernel - Bug #10025 (New): jessie: typing error: This oper...https://forge.ispras.ru/issues/100252020-01-09T16:29:42ZDenis Efremovefremov@ispras.ru
<pre>
$ frama-c -av is_successorless_vertex.c
[kernel] Parsing is_successorless_vertex.c (with preprocessing)
[av] Starting AstraVer translation
[av] Warning: \separated is not supported by AstraVer. This predicate will be ignored
[av] Producing files for AstraVer in subdir is_successorless_vertex.c.av
[av] File is_successorless_vertex.c.av/is_successorless_vertex_c.jc written.
[av] File is_successorless_vertex.c.av/is_successorless_vertex_c.cloc written.
[av] Calling AstraVer tool in subdir is_successorless_vertex.c.av
File "is_successorless_vertex_c.jc", line 116, characters 44-233: typing error: This operation on numeric values requires potentially unsafe or ambiguous type conversion that should be explicitly specified (the values' types are `uint64' and `int32')
[av] User Error: AstraVer subprocess failed: astraver -v -locs is_successorless_vertex_c.cloc is_successorless_vertex_c.jc
[kernel] Plug-in av aborted: invalid user input.
</pre> Deductive Verification Tools for Linux Kernel - Bug #10024 (New): jessie: typing error: numeric, ...https://forge.ispras.ru/issues/100242020-01-09T16:23:45ZDenis Efremovefremov@ispras.ru
<pre>
$ frama-c -av is_successorless_vertex.c
[kernel] Parsing is_successorless_vertex.c (with preprocessing)
[av] Starting AstraVer translation
[av] Warning: \separated is not supported by AstraVer. This predicate will be ignored
[av] Producing files for AstraVer in subdir is_successorless_vertex.c.av
[av] File is_successorless_vertex.c.av/is_successorless_vertex_c.jc written.
[av] File is_successorless_vertex.c.av/is_successorless_vertex_c.cloc written.
[av] Calling AstraVer tool in subdir is_successorless_vertex.c.av
File "is_successorless_vertex_c.jc", line 110, characters 44-226: typing error: numeric, boolean or pointer types expected for == and !=
[av] User Error: AstraVer subprocess failed: astraver -v -locs is_successorless_vertex_c.cloc is_successorless_vertex_c.jc
[kernel] Plug-in av aborted: invalid user input.
</pre> Deductive Verification Tools for Linux Kernel - Bug #10022 (New): internal error: named literals bughttps://forge.ispras.ru/issues/100222019-12-30T21:47:09ZDenis Efremovefremov@ispras.ru
<pre>
$ frama-c -av ghost_named_literals.c
[kernel] Parsing ghost_named_literals.c (with preprocessing)
[av] Starting AstraVer translation
[av] ghost_named_literals.c:22:10: Failure:
No matching literals found for proxy specification (variable proxy1)
[kernel] Current source was: ghost_named_literals.c:22
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 533, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1099, characters 17-55
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 526, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 529, characters 9-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2238, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml", line 3925, characters 28-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 2277, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2322, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3865, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6623, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6628, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6630, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2253, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6647, characters 15-39
Called from file "common.ml", line 1904, characters 4-148
Called from file "rewrite.ml", line 2505, characters 2-8
Called from file "rewrite.ml" (inlined), line 2509, characters 14-25
Called from file "rewrite.ml", line 2548, characters 2-81
Called from file "register.ml", line 146, characters 2-22
Called from file "register.ml", line 303, characters 6-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Plug-in av aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
</pre> Deductive Verification Tools for Linux Kernel - Bug #10021 (New): jessie: typing error: Unsupport...https://forge.ispras.ru/issues/100212019-12-30T17:28:03ZDenis Efremovefremov@ispras.ru
<pre>
frama-c -av list_init.c
</pre> Deductive Verification Tools for Linux Kernel - Bug #10020 (New): global names conflicthttps://forge.ispras.ru/issues/100202019-12-30T15:01:35ZDenis Efremovefremov@ispras.ru
<p>OK:<br /><pre>
$ frama-c -av -cpp-extra-args " -CC -E -D SPEC " ctype.h
$ frama-c -av -cpp-extra-args " -CC -E -D SPEC " ctype.c
$ frama-c -av -cpp-extra-args " -CC -E -D SPEC " ctype.h ctype.c
</pre></p>
<p>FAIL:<br /><pre>
$ frama-c -av -cpp-extra-args " -CC -E -D SPEC " ctype.c ctype.h
[kernel] Parsing ctype.c (with preprocessing)
[kernel] Parsing ctype.h (with preprocessing)
[kernel] ctype.h:126:3: Failure:
Literal proxy variable introduction failed: ctype_tbl
[kernel] User Error: skipping file ctype.h that has errors.
[kernel] Frama-C aborted: invalid user input.
</pre></p> Deductive Verification Tools for Linux Kernel - Bug #10019 (Open): LoopCurrent label supporthttps://forge.ispras.ru/issues/100192019-12-26T12:43:55ZDenis Efremovefremov@ispras.ru
<p>LoopCurrent support</p> Deductive Verification Tools for Linux Kernel - Bug #9709 (New): astraver: support calls annotationhttps://forge.ispras.ru/issues/97092019-06-14T15:48:07ZDenis Efremovefremov@ispras.ru
<pre>
static int parse_x509_signatureValue(const u8 *buf, u16 len,
const _alg_id *sig_alg, u16 *eaten)
{
int ret;
...
/*@ calls parse_sig_ecdsa, parse_sig_generic; @*/
ret = sig_alg->parse_sig(buf, len, eaten);
if (ret) {
ERROR_TRACE_APPEND(__LINE__);
goto out;
}
ret = 0;
out:
return ret;
}
</pre> Deductive Verification Tools for Linux Kernel - Bug #9708 (New): astraver: attach#global: called ...https://forge.ispras.ru/issues/97082019-06-14T15:46:07ZDenis Efremovefremov@ispras.ru
<pre>
[kernel] Parsing src/x509-parser.c (with preprocessing)
[av] Starting AstraVer translation
[av] src/x509-parser.c:9180:4: Failure:
attach#global: called on already dead object
[kernel] Current source was: src/x509-parser.c:9180
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 533, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1099, characters 17-55
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 526, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 529, characters 9-16
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1099, characters 4-125
Called from file "rewrite.ml", line 1636, characters 8-62
Called from file "rewrite.ml", line 1696, characters 24-41
Called from file "common.ml", line 107, characters 14-18
Called from file "common.ml" (inlined), line 113, characters 33-54
Called from file "rewrite.ml" (inlined), line 1693, characters 8-234
Called from file "rewrite.ml", line 1685, characters 10-570
Called from file "rewrite.ml", line 1706, characters 43-58
Called from file "list.ml", line 106, characters 12-15
Called from file "common.ml", line 1912, characters 4-26
Called from file "rewrite.ml", line 1742, characters 2-72
Called from file "rewrite.ml", line 2494, characters 2-8
Called from file "rewrite.ml" (inlined), line 2498, characters 14-25
Called from file "rewrite.ml", line 2509, characters 2-53
Called from file "register.ml", line 146, characters 2-22
Called from file "register.ml", line 303, characters 6-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
</pre> Deductive Verification Tools for Linux Kernel - Bug #9669 (New): verker: make sprove-proved, make...https://forge.ispras.ru/issues/96692019-05-22T07:27:18ZDenis Efremovefremov@ispras.ru
<p>VerKer master branch. make sprove-proved or make verify-proved hungs on goals generation.</p> Deductive Verification Tools for Linux Kernel - Bug #9600 (New): Why3Ide: "Fastest" button brokenhttps://forge.ispras.ru/issues/96002019-04-16T13:50:12ZDenis Efremovefremov@ispras.ru
<p>The "Fastest" button is not working.</p> Deductive Verification Tools for Linux Kernel - Feature #9598 (New): coq: driver: rewrite && to -...https://forge.ispras.ru/issues/95982019-04-15T17:10:32ZDenis Efremovefremov@ispras.ru
<p>Why3 generates definition for Count2 predicate:<br /><pre>
Inductive usCount2: (Pointer.pointer intP) -> Numbers.BinNums.Z -> Int32.t ->
Numbers.BinNums.Z -> (map.Map.map (Pointer.pointer intP) Int32.t) ->
Prop :=
| usNil : forall (intP_intM_a_2_at_L:(map.Map.map (Pointer.pointer intP)
Int32.t)), forall (a_0:(Pointer.pointer intP)), forall (v_0:Int32.t),
forall (n_2:Numbers.BinNums.Z), (n_2 <= 0%Z)%Z -> (usCount2 a_0 n_2 v_0
0%Z intP_intM_a_2_at_L)
| usHit : forall (intP_intM_a_2_at_L:(map.Map.map (Pointer.pointer intP)
Int32.t)), forall (a_1:(Pointer.pointer intP)), forall (v_1:Int32.t),
forall (n_3:Numbers.BinNums.Z), forall (sum_0:Numbers.BinNums.Z),
((0%Z < n_3)%Z /\ (((map.Map.get intP_intM_a_2_at_L (Pointer.shift a_1
(n_3 - 1%Z)%Z)) = v_1) /\ (usCount2 a_1 (n_3 - 1%Z)%Z v_1 sum_0
intP_intM_a_2_at_L))) -> (usCount2 a_1 n_3 v_1 (sum_0 + 1%Z)%Z
intP_intM_a_2_at_L)
| usMiss : forall (intP_intM_a_2_at_L:(map.Map.map (Pointer.pointer intP)
Int32.t)), forall (a_2:(Pointer.pointer intP)), forall (v_2:Int32.t),
forall (n_4:Numbers.BinNums.Z), forall (sum_1:Numbers.BinNums.Z),
((0%Z < n_4)%Z /\ ((~ ((map.Map.get intP_intM_a_2_at_L
(Pointer.shift a_2 (n_4 - 1%Z)%Z)) = v_2)) /\ (usCount2 a_2
(n_4 - 1%Z)%Z v_2 sum_1 intP_intM_a_2_at_L))) -> (usCount2 a_2 n_4 v_2
sum_1 intP_intM_a_2_at_L).
</pre></p>
<p>Vanilla Frama-C simplifies this to (->, let):<br /><pre>
Inductive P_Count2 : farray addr Z -> addr -> Z -> Z -> Z -> Prop :=
| Q_Nil: forall (i_1 i : Z), forall (t : farray addr Z),
forall (a : addr), ((i <= 0)%Z) -> ((is_sint32 i_1%Z)) ->
((P_Count2 t a i%Z i_1%Z 0%Z))
| Q_Hit: forall (i_1 i : Z), forall (t : farray addr Z),
forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((0 < i_1)%Z) ->
((is_sint32 x_1)) -> ((P_Count2 t a x x_1 i%Z)) ->
((P_Count2 t a i_1%Z x_1 (1%Z + i%Z)%Z))
| Q_Miss: forall (i_2 i_1 i : Z), forall (t : farray addr Z),
forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
(((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((0 < i_1)%Z) ->
((is_sint32 i_2%Z)) -> ((P_Count2 t a x i_2%Z i%Z)) ->
((P_Count2 t a i_1%Z i_2%Z i%Z)).
</pre></p>
<p>Thus, the original deifinition:<br /><pre>
inductive Count2{L}(value_type *a, integer n, value_type v, integer sum) {
case Nil{L}:
\forall value_type *a, v, integer n;
n <= 0 ==>
Count2{L}(a, n, v, 0);
case Hit{L}:
\forall value_type *a, v, integer n, sum;
0 < n && a[n-1] == v && Count2{L}(a, n-1, v, sum) ==>
Count2{L}(a, n, v, sum + 1);
case Miss{L}:
\forall value_type *a, v, integer n, sum;
0 < n && a[n-1] != v && Count2{L}(a, n-1, v, sum) ==>
Count2{L}(a, n, v, sum);
}
</pre></p>
<p>simplified to:<br /><pre>
inductive Count2{L}(value_type *a, integer n, value_type v, integer sum) {
case Nil{L}:
\forall value_type *a, v, integer n;
n <= 0 ==>
Count2{L}(a, n, v, 0);
case Hit{L}:
\forall value_type *a, v, integer n, sum;
\let n1 = n - 1;
\let an = a[n1];
0 < n ==> Count2{L}(a, n1, an, sum) ==>
Count2{L}(a, n, an, sum + 1);
case Miss{L}:
\forall value_type *a, v, integer n, sum;
\let n1 = n - 1;
0 < n ==> a[n1] != v ==> Count2{L}(a, n1, v, sum) ==>
Count2{L}(a, n, v, sum);
}
</pre></p>
<p>After the simplification the Coq proof can be as short as:<br /><pre>
intros. induction H; auto with zarith.
</pre></p>