frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-07-21T13:01:36Zhttps://git.frama-c.com/pub/frama-c/-/issues/2632-wp-print for only failed goals2023-07-21T13:01:36ZDavid Cok-wp-print for only failed goalsI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2631Naming the anonymous behavior for -wp-bhv2023-06-21T08:58:19ZDavid CokNaming the anonymous behavior for -wp-bhvFeature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax tha...Feature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax that does not interfere with most shells. For example -wp-bhv ~Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2630Ghost variable initialization and logic functions2022-09-01T06:31:17ZDavid CokGhost variable initialization and logic functions
### Steps to reproduce the issue
Here is example code:
```
/*@ axiomatic A {
logic integer Lneg(integer i) = -i;
}
*/
/*@ assigns \nothing; ensures \result == -i; */
int neg(int i) { return -i; }
void test(int j) {
//@ ghost i...
### Steps to reproduce the issue
Here is example code:
```
/*@ axiomatic A {
logic integer Lneg(integer i) = -i;
}
*/
/*@ assigns \nothing; ensures \result == -i; */
int neg(int i) { return -i; }
void test(int j) {
//@ ghost int kk = Lneg(j);
int k = neg(j);
//@ assert k == kk;
}
```
`frama-c -wp` produces
```
fc $ frama-c -wp logic.c
[kernel] Parsing logic.c (with preprocessing)
[kernel:typing:implicit-function-declaration] logic.c:10: Warning:
Calling undeclared function Lneg. Old style K&R code?
[kernel:ghost:bad-use] logic.c:10: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:annot:missing-spec] logic.c:9: Warning:
Neither code nor specification for function Lneg, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_test_assert : Timeout (Qed:1ms) (10s)
[wp] Proved goals: 2 / 3
Qed: 2 (0.21ms-0.72ms)
Alt-Ergo 2.4.1: 0 (interrupted: 1)
[wp:pedantic-assigns] logic.c:9: Warning:
No 'assigns' specification for function 'test'.
Callers assumptions might be imprecise.
[wp:pedantic-assigns] logic.c:10: Warning:
No 'assigns' specification for function 'Lneg'.
Callers assumptions might be imprecise.
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```
It appears to treat Lneg as a regular function, complaining that it is non-ghost and has no specs.
However, if `neg` is used instead, WP still complains, although now it runs the proof successfully:
```
[kernel] Parsing logic.c (with preprocessing)
[kernel:ghost:bad-use] logic.c:10: Warning:
Call to non-ghost function from ghost code is not allowed
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] Proved goals: 3 / 3
Qed: 3 (0.21ms-0.68ms-1ms)
[wp:pedantic-assigns] logic.c:9: Warning:
No 'assigns' specification for function 'test'.
Callers assumptions might be imprecise.
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```
### Expected behaviour
I would expect `Lneg` to be allowed here. If a non-ghost function like `neg` is allowed to be used as a ghost logic function, as it apparently is (e.g. as long as it is pure), then there should be no need for a warning.
### Contextual information
Frama-C 25.0, built from source, with frama-clang added. Using WP as built with Frama-C.
MacOS 12.5Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2629Anomalous behavior of anonymous 'behavior'2022-09-22T08:58:47ZDavid CokAnomalous behavior of anonymous 'behavior'
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
...
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
/*@
requires P != 0;
assigns Q;
ensures Q == 1;
*/
void d() {
Q = 1;
}
//@ assigns Q;
void c() {
d();
}
```
which is an minimal as I could make it.
Note that a calls b, where b has a always-true behavior. c calls d the same way, but without a behavior.
The example is extracted from a larger specification with lots of behaviors.
### Actual behaviour
In my environment, the above, run with `frama-c -wp` produces
```
fc $ frama-c -wp behavior.c
[kernel] Parsing behavior.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_exit : Timeout (Qed:0.81ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_call_b_requires : Timeout (Qed:0.78ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_normal : Timeout (Qed:0.77ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_c_call_d_requires : Timeout (10s)
[wp] Proved goals: 7 / 11
Qed: 7
Alt-Ergo 2.4.1: 0 (interrupted: 4)
```
That is c calling d is fine. a calling b is not.
### Expected behaviour
I expect a calling be to behave precisely like c calling d.
It appears that even with a prefix consisting of just requires clauses, WP produces an
anonymous behavior that contains something like `assigns \everything`. That then causes
the very mysterious assigns errors that you see above.
Fortunately, now that I know the problem there is an easy workaround -- but prior to that it wasted many days of time.
### Contextual information
Frama-C 25.0, built from source, with WP
MacOS 12.5Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2628syntax error for using bool datatype (stdbool.h) for C code analysis2022-08-25T21:30:46Zankit247syntax error for using bool datatype (stdbool.h) for C code analysishttps://stackoverflow.com/questions/73485749/frama-c-compilation-issue-for-bool
The code is compiling with gcc compiler. But with framac, I am having issue using bool data type from stdbool.h
I have started using framac just last week,...https://stackoverflow.com/questions/73485749/frama-c-compilation-issue-for-bool
The code is compiling with gcc compiler. But with framac, I am having issue using bool data type from stdbool.h
I have started using framac just last week, is it I am missing include path.https://git.frama-c.com/pub/frama-c/-/issues/2627error about e-acsl-gcc.sh syntax error2022-08-23T01:29:31ZJaeD-Shinerror about e-acsl-gcc.sh syntax errorI run `e-acsl-gcc.sh -c ./*` for the whole directory, but it does not proceed with the following error. Is there any way to find out what the problem is?
```
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h ...I run `e-acsl-gcc.sh -c ./*` for the whole directory, but it does not proceed with the following error. Is there any way to find out what the problem is?
```
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body ./ABOUT-NLS ./aclocal.m4 ./AUTHORS ./autom4te.cache ./build-aux ./cfg.mk ./ChangeLog ./ChangeLog-2009 ./config.h ./config.hin ./config.hin~ ./config.log ./config.status ./configure ./configure.ac ./COPYING ./dist-check.mk ./doc ./err ./err.txt ./gnulib-tests ./GNUmakefile ./INSTALL ./lib ./m4 ./maint.mk ./Makefile ./Makefile.am ./Makefile.in ./MVIV1.txt ./NEWS ./po ./README ./README-alpha ./src ./stamp-h1 ./tests ./THANKS ./thanks-gen ./THANKS.in ./TODO -o a.out
/usr/bin/ld:./ABOUT-NLS: file format not recognized; treating as linker script
/usr/bin/ld:./ABOUT-NLS:1: syntax error
collect2: error: ld returned 1 exit status
```https://git.frama-c.com/pub/frama-c/-/issues/2626Install error2022-08-29T09:40:44Zalicorn0618Install error<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
follow the recommended ways of installing Frama-c on Mac
### Expected behaviour
Install frama-c successfully
### Actual behaviour
Errors in installing Frama-C
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 25.0
- Plug-in used: *Plug-in used*
- OS name: MacOS X64
- OS version: Monterey 12.5.1
### Additional information (optional)
when I use command
```
opam install frama-c
```
Errors will be raised like
```
The following actions will be performed:
- install frama-c 25.0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved frama-c.25.0 (cached)
[ERROR] The compilation of frama-c.25.0 failed at "make -j11".
#=== ERROR while compiling frama-c.25.0 =======================================#
# context 2.1.3 | macos/x86_64 | ocaml-base-compiler.4.12.0 | https://opam.ocaml.org#cb4d2b35
# path ~/.opam/cs3110-2021fa/.opam-switch/build/frama-c.25.0
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j11
# exit-code 2
# env-file ~/.opam/log/frama-c-25672-338565.env
# output-file ~/.opam/log/frama-c-25672-338565.out
### output ###
# [...]
# make: *** [share/Makefile.generic:78: src/plugins/aorai/promelaoutput.cmo] Error 2
# make: *** [share/Makefile.generic:78: src/plugins/aorai/bool3.cmo] Error 2
# File "src/plugins/aorai/data_for_aorai.ml", line 26, characters 5-16:
# 26 | open Logic_ptree
# ^^^^^^^^^^^
# Error: Unbound module Logic_ptree
# File "src/plugins/aorai/aorai_utils.ml", line 26, characters 5-8:
# 26 | open Cil
# ^^^
# Error: Unbound module Cil
# make: *** [share/Makefile.generic:78: src/plugins/aorai/data_for_aorai.cmo] Error 2
# make: *** [share/Makefile.generic:78: src/plugins/aorai/aorai_utils.cmo] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build frama-c 25.0
+-
- No changes have been performed
<><> frama-c.25.0 troubleshooting <><><><><><><><><><><><><><><><><><><><><><><>
=> Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect
```https://git.frama-c.com/pub/frama-c/-/issues/2625Frama-c crash in ast_queries/ast_info.ml with unexpected error2022-08-31T08:53:08ZKarine EMFrama-c crash in ast_queries/ast_info.ml with unexpected error<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
frama-c -eva test.c
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Frama-c crashed on this C file:
```
void main() { char a[1][3 % 1] = {'3'}; }
```
with this error:
```
Unexpected error (File "src/kernel_services/ast_queries/ast_info.ml", line 53, characters 12-18: Assertion failed).
```
If I simplify the expression "3 % 1" to 1, the code no long crash frama-c.
### Contextual information
- Frama-C installation mode: *Opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 20.04.1 x86_64
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
The trace of the crash:
```
[kernel] Current source was: test.c:1
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/ast_info.ml", line 53, characters 12-24
Called from file "src/kernel_services/ast_queries/ast_info.ml", line 416, characters 41-60
Called from file "src/plugins/inout/cumulative_analysis.ml", line 36, characters 9-32
Called from file "src/plugins/inout/operational_inputs.ml", line 412, characters 25-73
Called from file "src/plugins/inout/operational_inputs.ml", line 454, characters 34-59
Called from file "src/kernel_services/analysis/dataflows.ml", line 515, characters 12-42
Called from file "src/kernel_services/analysis/dataflows.ml", line 523, characters 19-30
Called from file "src/kernel_services/analysis/dataflows.ml", line 524, characters 5-14
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 583, characters 10-48
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 583, characters 10-57
Called from file "src/kernel_services/analysis/dataflows.ml", line 583, characters 10-60
Called from file "src/plugins/inout/operational_inputs.ml" (inlined), line 695, characters 6-37
Called from file "src/plugins/inout/operational_inputs.ml", line 695, characters 6-48
Called from file "src/plugins/inout/operational_inputs.ml", line 706, characters 15-79
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/plugins/value/engine/iterator.ml", line 732, characters 8-214
Called from file "src/plugins/value/engine/iterator.ml", line 781, characters 6-42
Called from file "src/plugins/value/utils/eva_utils.ml", line 121, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml" (inlined), line 214, characters 17-68
Called from file "src/plugins/value/engine/compute_functions.ml", line 247, characters 8-47
Called from file "src/plugins/value/engine/compute_functions.ml", line 252, characters 38-63
Called from file "src/plugins/value/engine/compute_functions.ml", line 178, characters 24-54
Called from file "src/plugins/value/engine/compute_functions.ml", line 358, characters 25-66
Called from file "src/plugins/value/utils/eva_utils.ml", line 121, characters 6-10
Called from file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from file "src/plugins/value/register.ml", line 31, characters 40-59
Called from file "queue.ml", line 121, 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 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/kernel_services/ast_queries/ast_info.ml", line 53, characters 12-18: Assertion failed).
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2624Dependencies for building frame-clang on Ubuntu are incomplete or wrong2022-08-24T09:50:37ZDavid CokDependencies for building frame-clang on Ubuntu are incomplete or wrong
On Ubuntu, either 18.04 or 20.04
the description of dependencies for building frame-clang is incomplete.
With llvm@14 installed (with brew)
and frama-c 24 installed (with opam)
frame-clang fails to build or run (variously compile fail...
On Ubuntu, either 18.04 or 20.04
the description of dependencies for building frame-clang is incomplete.
With llvm@14 installed (with brew)
and frama-c 24 installed (with opam)
frame-clang fails to build or run (variously compile failures, link failures and failure to find .so at runtime)
unless also gcc/g++ -12 is installed (gcc-11 and gcc-10 at least both fail).
Even so, there are warnings during the build of frama-clang.
Also, I suspect that frame-clang is not buildable with earlier versions of llvm, but I did not exhaustively search for an appropriate version of gcc.
Note that https://frama-c.com/fc-plugins/frama-clang.html does say that frama-clang 0.0.12 depends on Frama-c 24 (correctly), but claims any clang above 10 is OK. I don't think that is correct, but if it is, each clang version should state which g++ version is required.
But the frame-clang manual linked on that page (https://frama-c.com/download/frama-clang-manual.pdf) points to frame-clang version 0.0.10 and Frama-C 22.https://git.frama-c.com/pub/frama-c/-/issues/2623Unexpected error when using/typecasting _Bool types2022-08-31T14:43:19ZT-GruberUnexpected error when using/typecasting _Bool typesThe following code crashed with an unexpected error.
### Steps to reproduce the issue
```
_Bool get_bool(void);
_Bool pass_bool(_Bool b);
_Bool b_flag1, b_flag2;
void main(){
b_flag1 = pass_bool( !(_Bool)get_bool() );
b_flag...The following code crashed with an unexpected error.
### Steps to reproduce the issue
```
_Bool get_bool(void);
_Bool pass_bool(_Bool b);
_Bool b_flag1, b_flag2;
void main(){
b_flag1 = pass_bool( !(_Bool)get_bool() );
b_flag2 = pass_bool( (_Bool)get_bool() );
}
> frama-c -deps bool_fails.i
```
### Expected behaviour
```
.
.
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function get_bool:
\result FROM \nothing
[from] Function pass_bool:
\result FROM b
[from] Function main:
b_flag1 FROM \nothing
b_flag2 FROM \nothing
[from] ====== END OF DEPENDENCIES ======
```
### Actual behaviour
```
[from] Computing for function main
[from] Computing for function get_bool <-main
[from] Done for function get_bool
[from] Computing for function pass_bool <-main
[kernel] Current source was: bool_fails.i:10
The full backtrace is:
Raised at Offsetmap.Make.merge in file "src/kernel_services/abstract_interp/offsetmap.ml", line 945, characters 23-35
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Offsetmap.Make.merge in file "src/kernel_services/abstract_interp/offsetmap.ml", line 999, characters 10-57
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Offsetmap.Make.join in file "src/kernel_services/abstract_interp/offsetmap.ml", line 1222, characters 15-62
Called from Hptmap.Make.join.decide_both in file "src/libraries/utils/hptmap.ml", line 1195, characters 14-37
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Hptmap.Make.generic_merge.merge_branches in file "src/libraries/utils/hptmap.ml", line 1131, characters 17-28
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Hptmap.Make.generic_merge.merge_branches in file "src/libraries/utils/hptmap.ml", line 1131, characters 17-28
Called from Binary_cache.Symmetric_Binary.merge in file "src/libraries/utils/binary_cache.ml", line 275, characters 19-26
Called from Lmap.Make_LOffset.join in file "src/kernel_services/abstract_interp/lmap.ml", line 688, characters 41-55
Called from Stdlib__Hashtbl.fold.do_bucket in file "hashtbl.ml", line 211, characters 23-40
Called from Stdlib__Hashtbl.fold in file "hashtbl.ml", line 218, characters 14-35
Re-raised at Stdlib__Hashtbl.fold in file "hashtbl.ml", line 224, characters 4-13
Called from Db.Value.get_initial_state in file "src/kernel_services/plugin_entry_points/db.ml", line 503, characters 10-140
Called from From_compute.Make.compute_using_prototype in file "src/plugins/from/from_compute.ml", line 674, characters 16-45
Called from From_compute.Make.compute_and_return in file "src/plugins/from/from_compute.ml", line 693, characters 11-37
Called from From_compute.Make.compute in file "src/plugins/from/from_compute.ml", line 705, characters 11-34
Called from Functionwise.To_Use.memo.(fun) in file "src/plugins/from/functionwise.ml", line 45, characters 9-26
Called from State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from From_compute.Make.Computer.transfer_call.do_on in file "src/plugins/from/from_compute.ml", line 383, characters 27-55
Called from From_compute.Make.Computer.transfer_call in file "src/plugins/from/from_compute.ml", line 444, characters 17-65
Called from From_compute.Make.Computer.transfer_stmt in file "src/plugins/from/from_compute.ml", line 535, characters 36-61
Called from Dataflows.Forward_monotone_generic_storage.do_stmt in file "src/kernel_services/analysis/dataflows.ml", line 515, characters 12-42
Called from Dataflows.Forward_monotone_generic_storage.compute in file "src/kernel_services/analysis/dataflows.ml", line 523, characters 19-30
Called from Dataflows.Forward_monotone_generic_storage in file "src/kernel_services/analysis/dataflows.ml", line 524, characters 5-14
Called from Dataflows.Simple_forward in file "src/kernel_services/analysis/dataflows.ml" (inlined), line 583, characters 10-48
Called from Dataflows.Simple_forward in file "src/kernel_services/analysis/dataflows.ml" (inlined), line 583, characters 10-57
Called from Dataflows.Simple_forward in file "src/kernel_services/analysis/dataflows.ml", line 583, characters 10-60
Called from From_compute.Make.compute_using_cfg.Compute in file "src/plugins/from/from_compute.ml" (inlined), line 634, characters 31-61
Called from From_compute.Make.compute_using_cfg.Compute in file "src/plugins/from/from_compute.ml", line 634, characters 31-75
Called from From_compute.Make.compute_and_return in file "src/plugins/from/from_compute.ml", line 694, characters 11-31
Called from From_compute.Make.compute in file "src/plugins/from/from_compute.ml", line 705, characters 11-34
Called from Functionwise.To_Use.memo.(fun) in file "src/plugins/from/functionwise.ml", line 45, characters 9-26
Called from State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from Functionwise.(fun) in file "src/plugins/from/functionwise.ml", line 106, characters 22-38
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from From_register.main.(fun) in file "src/plugins/from/from_register.ml", line 151, characters 9-32
Called from From_register.main in file "src/plugins/from/from_register.ml", line 149, characters 4-119
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/offsetmap.ml", line 945, characters 23-29: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 25.0-beta (Manganese).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: opam installation
- Frama-C version: 25.0-beta (Manganese)
- OS name: Ubuntu (WSL)
### Additional information (optional)
There are some modifications that prevent the program from a crash. Some examples are:
- remove the negation in the first call of pass_bool
- remove one of the calls to pass_bool, does not matter which one
- remove the typecast (_Bool) inside the call to pass_bool
- use temporary variables for the return value from get_bool and pass that variables to pass_boolVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2622Missing master download page2022-08-10T09:46:43ZJulien PuydtMissing master download pageThe web site for frama-c changed ; there was a nice download.html page with direct links to versioned .tar.gz source tarballs.
Now you have to navigate through pages to find the latest version : [this first page](https://frama-c.com/htm...The web site for frama-c changed ; there was a nice download.html page with direct links to versioned .tar.gz source tarballs.
Now you have to navigate through pages to find the latest version : [this first page](https://frama-c.com/html/get-frama-c.html) gives you a direct link to an unnumbered last-version tarball, and [this second page](https://frama-c.com/html/framac-versions.html) will give you different links to pages about the various versions.
It's just a little tedious for a human, but it's really awful for automated checks, like what distributions use to get notified and easily download new source versions.
Case in point, in Debian, we have the following file to detect versions:
```
version=4
opts="dversionmangle=s/[0-9]+\+([a-z]+)/$1/i" \
https://frama-c.com/download.html download/frama-c-[0-9]{2}\.[0-9]-([a-zA-Z]+)\.tar\.gz
```
and until now it was automatically notifying us there was a new version to package, and when we wanted to package it, it could download it for us without poking around.
Could you put back a download.html page with direct links?
ThanksAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2621[Frama-C/WP] The history of internal state changes VC goal outcomes2022-09-26T13:49:51Zstephengaito[Frama-C/WP] The history of internal state changes VC goal outcomes### Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: `code/function-contract/contract/ex-3-alphabet-answer.c`)...
Start `frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c`.
Right-...### Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: `code/function-contract/contract/ex-3-alphabet-answer.c`)...
Start `frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c`.
Right-click on the function prototype `int alphabet_letter` and select `Prove function annotations by WP`, the first VC (`ensures`) should fail.
Right-click on the function prototype `int alphabet_letter` a second time and select `Prove function annotations by WP`, the first VC (`ensures`) should succeed.
### Expected behaviour
The order in which WP proof invocations *should* *not* change the VC goal outcomes if there is no change to the underlying code/annotations.
### Actual behaviour
The history of WP proof invocations does seem to change the VC goal outcomes.
### Contextual information
- Frama-C, Why3, Alt-Ergo installation mode: *all via Opam*
- Frama-C version: *25.0-beta (Manganese)*
- Plug-in used: *WP*
- Why3 version: *Why3 platform, version 1.5.0*
- Alt-Ergo version: *2.4.1*
- OS name: *Ubuntu*
- OS version: *21.10 (Impish)*
- Number of CPU's: *2*
- CPU speed: *2.80GHz*
- RAM: *16Gb*Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2620[WP] There is no obvious way to exit the Interactive Proof Editor (and return...2022-06-30T16:02:25Zstephengaito[WP] There is no obvious way to exit the Interactive Proof Editor (and return to the list of WP goals).### Steps to reproduce the issue
Running frama-c-gui apply WP to a function with multiple VCs and open the "WP Goals" and click on *one* of the VCs.
### Expected behaviour
I expect to find a button or a right-click menu item which all...### Steps to reproduce the issue
Running frama-c-gui apply WP to a function with multiple VCs and open the "WP Goals" and click on *one* of the VCs.
### Expected behaviour
I expect to find a button or a right-click menu item which allows me to close the Interactive Proof Editor on the "current VC" and return to the List of WP Goals. (IE. I can find no way to switch from a detailed VC view back to the overall list of Goals view).
### Actual behaviour
I can find no such button or right-click menu item while "inside" the Interactive Proof Editor.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *25.0-beta (Manganese)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *21.10 (Impish)*
### Additional information (optional)
I have found that:
1. I can switch between VCs in the Interactive Proof Editor by using the mouse to click on different ensures or asserts in the normalized code text.
2. I can recover the overall list of WP goals IF I manage to click on an ensure or assertion which is not in the "currently selected" "Not Proven (yet)" goals list... (If I have an assertion which *has* been proven).
Unfortunately I would like/expect a direct way to exit the Interactive Proof Editor and return to the list of WP Goals.https://git.frama-c.com/pub/frama-c/-/issues/2619correspondance → correspondence2022-09-27T16:40:42ZDimitri Papadopoulos Orfanoscorrespondance → correspondenceIn file [`src/kernel_services/ast_queries/ast_diff.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/kernel_services/ast_queries/ast_diff.mli) / [`src/kernel_services/ast_queries/ast_diff.ml`](https://git.frama-c.com/pub/frama-...In file [`src/kernel_services/ast_queries/ast_diff.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/kernel_services/ast_queries/ast_diff.mli) / [`src/kernel_services/ast_queries/ast_diff.ml`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/kernel_services/ast_queries/ast_diff.ml), you should change _correspondance_ (French) to _correspondence_ (English).
Not sure of the impact of such a change, which is why I don't suggest a patch.https://git.frama-c.com/pub/frama-c/-/issues/2618[Feature Request] Add original src line number in WP proof obligation files.2022-06-24T08:56:04Zstephengaito[Feature Request] Add original src line number in WP proof obligation files.Hello,
I am trying to understand why WP is having problems with a 'simple' `calloc` of a complex (ie non-int) memory structure. (This is something done fairly often in ANSI-C code).
AND *yes* I realize that raw C pointers are dangerous...Hello,
I am trying to understand why WP is having problems with a 'simple' `calloc` of a complex (ie non-int) memory structure. (This is something done fairly often in ANSI-C code).
AND *yes* I realize that raw C pointers are dangerous and hence make WP's job nearly impossible... so I *do* expect that I need to 'teach' WP something about *my* use of pointers. Unfortunately, at the moment, I am at a loss as to what additional information I need to provide to WP.
(I *have* repeatedly (re)read the various "Memory Model" / "Dynamic Allocation" sections of the ACSL, EVA and WP manuals... )
While researching this problem, I noticed that Frama-C has an `-wp-out <directory>` switch which can be used to keep all of WP's proof obligations for review by human inspection / interaction with the Why3 gui.
When I added this switch, I find a large number of individual files with Why3/Alt-Ergo statements in them.
**Unfortunately** I am not experienced enough with the system to map each file to the particular WP assertion in the original source code that WP is trying to prove.
**Request:** Could you add a simple one line comment `(* ... *)` at the top of each of the proof obligation files which informs a human reader which original line of source code and/or rte/wp assertion (in ACSL) is being proven?
This would help a non-Frama-C developer by providing the conceptual context for the proof obligation being proven.
Regards, Stephen GaitoLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2617[WP] The support of sets is partial2023-02-06T11:02:59ZYani ZIANI[WP] The support of sets is partial<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Running Frama-C with WP on the following code after uncommenting any of the designated lines. The main idea here was to try and represent a basic C linked list structure as an ACSL tset to easy reasoning and benefit from already existing ACSL clauses.
```C
#include <stdio.h>
typedef struct NODE_TEST {
int handle;
struct NODE_TEST * next;
} NODE_TEST;
/**
* Reachability in linked lists as defined in the ACSL language implementation
* on the Frama-C website
*/
/*@ inductive reachable_node_t{L}(NODE_TEST *root, NODE_TEST *to) {
case empty{L}:
\forall NODE_TEST *l; reachable_node_t{L}(l,l) ;
case non_empty{L}: \forall NODE_TEST *l1,*l2;
\valid(l1)
&& reachable_node_t{L}(l1->next,l2)
==> reachable_node_t{L}(l1,l2) ;
@}
*/
/**
* Logic function used to tranlate a C linked list of NODE_TEST into an ASCL
* tset of its nodes (or at least an attempt at making one). The aim here
* would be to store each pointer to each node of a given linked list in a
* ACSL structure in order to facilitate the proofs of properties such as
* memory separation (by applying the \separated clause to the whole tset),
* loop invariants (using, for instance, the existing \in clause for tsets),
* and others.
*/
/*@ axiomatic NodeTestTSet {
logic set<NODE_TEST *> node_to_tset{L}(NODE_TEST *node)
reads { nod->next | struct NODE_TEST* nod ;
reachable_node_t{L}(nod, \null) && nod \in node_to_tset(node) };
axiom node_empty_tset{L}:
\forall NODE_TEST *node;
node == \null
==> node_to_tset{L}(node) == \empty;
axiom node_not_empty_tset{L}:
\forall NODE_TEST *node;
\let tail = node_to_tset{L}(node->next);
( \valid(node) && reachable_node_t{L}(node->next, \null) )
==> node_to_tset{L}(node) == \union({node}, tail);
}
*/
/**
* Axiomatic definition of the length of a well typed linked list
*/
/*@ axiomatic NodeTestListLgth {
logic integer node_lgth{L}(NODE_TEST *node)
reads { nod->next | struct NODE_TEST* nod; nod \in node_to_tset(node) } ;
axiom node_empty_lgth{L}:
\forall NODE_TEST *node;
node == \null ==> node_lgth{L}(node) == 0;
axiom node_t_not_empty_lgth{L}:
\forall NODE_TEST * node;
(node != \null
&& reachable_node_t{L}(node, \null) )
==> node_lgth{L}(node) == node_lgth{L}(node->next) + 1;
}
*/
/**
* Predicates to easy readability
*/
/*@ predicate is_handle_in_list_tset{L}(NODE_TEST *root, int out_handle) =
\exists NODE_TEST *node;
node \in node_to_tset(root) && node->handle == out_handle;
*/
/*@ predicate is_handle_in_list_reach{L}(NODE_TEST *root, int out_handle) =
\exists NODE_TEST *node;
reachable_node_t(root, node) && node->handle == out_handle;
*/
/*****************************************************************/
/*@
requires linked_list != \null && reachable_node_t(linked_list,\null);
requires 0 < node_lgth(linked_list) <= 10000;
behavior handle_in_list:
// assumes is_handle_in_list_tset(linked_list, out_handle); //causes a why3 error when uncommented
assumes is_handle_in_list_reach(linked_list, out_handle);
ensures \result == 616;
behavior handle_not_in_list:
// assumes !(is_handle_in_list_tset(linked_list, out_handle)); //causes a why3 error when uncommented
assumes !(is_handle_in_list_reach(linked_list, out_handle));
ensures \result == 1610;
disjoint behaviors;
complete behaviors;
*/
int getNode(NODE_TEST * linked_list, int out_handle) {
NODE_TEST *temp_node;
/*@ ghost int n = 0;*/
/*@
loop invariant 0 <= n <= node_lgth(linked_list);
loop invariant temp_node \in node_to_tset(linked_list); //causes a why3 error when uncommented
loop invariant reachable_node_t(linked_list, temp_node);
loop invariant reachable_node_t(temp_node, \null);
loop assigns n, temp_node;
loop variant node_lgth(linked_list) + 1 - n;
*/
for (temp_node = linked_list; temp_node != NULL;
temp_node = temp_node->next) {
if (temp_node->handle == out_handle)
return 616;
/*@ghost n++;*/
}
return 1610;
}
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
Proofs of properties ending either successfully or with a timeout.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Most proofs end up failing with a why3 error ``[Why3 Error] Library file not found: vset``, even those pertaining to properties that would be proven without the "problematic" lines.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 22.0 (Titanium), 23.0 (Vanadium), 23.1 (Vanadium), *24.0 (Chromium)* and *25.0-beta (Manganese)* (as reported by `frama-c -version`)
- Plug-in used: WP (using Qed and Alt-Ergo)
- OS name: *Ubuntu*
- OS version: *20.04.4 LTS*
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
In the case of Frama-C 24, I also did try using both versions 2.3.2 and 2.4.1 of Alt-Ergo, Frama-C 25 was tested using Alt-Ergo 2.4.1, and every other versions of Frama-C used v2.3.2.
FYI @nkosmatovAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2616`frama-c-script build` NEEDS Blug installed... where do I get Blug?2022-06-16T18:43:10Zstephengaito`frama-c-script build` NEEDS Blug installed... where do I get Blug?Hello,
I am trying to run `frama-c-script build` in a directory which has a valid `compile_commands.json` file.
I am getting the following error:
> frama-c-script build
> error: path to 'blug' binary must be in PATH or variable BLUG...Hello,
I am trying to run `frama-c-script build` in a directory which has a valid `compile_commands.json` file.
I am getting the following error:
> frama-c-script build
> error: path to 'blug' binary must be in PATH or variable BLUG
I can find nowhere in your documentation, your various blog articles, nor any issues about where I should get and/or how I should install `Blug`.
(I see from the source code for `share/analysis-scripts/build.py` that the only uses of `blug` are the `blug_jbdb` and `prettify` sub-code... I can find no `blug` project (on opam nor PyPi.com) which contains these "symbols").
Where can I find this Python script/module?
Regards, Stephen GaitoAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2615compilation of Frama-C 25.0~beta does not stop on macOS2022-07-08T08:35:32ZJens Gerlachcompilation of Frama-C 25.0~beta does not stop on macOSBoth on macOS 12.4 and macOS 11.6.6 the compilation of Frama-C 25.0~beta does not stop (even when running for hours).
Here are some details on my opam installation on macOS 12.4
opam-version: "2.0"
opam-root-version: "2.1"
repositories:...Both on macOS 12.4 and macOS 11.6.6 the compilation of Frama-C 25.0~beta does not stop (even when running for hours).
Here are some details on my opam installation on macOS 12.4
opam-version: "2.0"
opam-root-version: "2.1"
repositories: "default"
installed-switches: "4.13.1"
switch: "4.13.1"
Hope this helps!https://git.frama-c.com/pub/frama-c/-/issues/2614Asking the UI to evaluate an invalid ACSL term makes the UI crash2022-06-10T07:42:41ZAlexCidAsking the UI to evaluate an invalid ACSL term makes the UI crash<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
Open the UI (using at least the EVA plugin) to analyze any file, right-click almost anywhere, select "Evaluate ACSL term" and enter any invalid ACSL term.
### Expected behaviour
The UI should display a warning but continue to be usable afterwards.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
The following dialog is shown:
"Error: Invalid term: Unbound variable azerty" (for example), and then:
```
Error
Current source was filename.c:lineno
The full backtrace is:
Raised at file "map.ml", line 135, characters 10-25
Called from file "src/plugins/value/engine/abstractions.ml" line 96, characters 19-61
Unexpected error (Failure("dialog destroyed")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
...
```
After that, trying to evaluate _any_ ACSL term summons that same dialog.
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: docker image
- Frama-C version: 24.0
- Plug-in used: ?
- OS name: Linux
- OS version: Ubuntu 20.04https://git.frama-c.com/pub/frama-c/-/issues/2613Questions about other function2022-07-12T06:53:28ZJaeD-ShinQuestions about other functionI have a question.
Is there a function to save the output from the `e-acsl-gcc.sh` command as a log(or txt) file ?I have a question.
Is there a function to save the output from the `e-acsl-gcc.sh` command as a log(or txt) file ?Julien SignolesJulien Signoles