frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-28T11:13:02Zhttps://git.frama-c.com/pub/frama-c/-/issues/128Syntax error in reorder_defs.ml after running make2022-09-28T11:13:02Zmantis-gitlab-migrationSyntax error in reorder_defs.ml after running makeID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002480 | Frama-C | Plug-in > clang | public | 2019-10-03 | 2019-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gpajela | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Ubuntu | **OS Version** | 18.04.3 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to follow the instructions at https://frama-c.com/frama-clang.html to install Frama-Clang. However, I get a "Syntax error" after I run make:
$ make
Generating .Makefile.plugin.generated
Ocamlc intermediate_format.cmi
Ocamlc intermediate_format_parser.cmi
Ocamlc intermediate_format_parser.cmo
Ocamlc frama_Clang_option.cmi
Ocamlc frama_Clang_option.cmo
Ocamlc fclang_datatype.cmi
Ocamlc fclang_datatype.cmo
Ocamlc reorder_defs.cmi
Ocamlc reorder_defs.cmo
File "reorder_defs.ml", line 310, characters 6-10:
Error: Syntax error
/data/loewenheim/a/gpajela/.opam/default/share/frama-c/Makefile.generic:77: recipe for target 'reorder_defs.cmo' failed
make: *** [reorder_defs.cmo] Error 2
### Additional Information :
I am using Frama-C 19.0 Potassium, which I installed using opam pin. I am using version 2.0.4 of opam. I am using the default versions of OCaml and Clang for this version of Ubuntu: OCaml 4.05.0 and clang version 6.0.0.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/135E-ACSL: segmentation fault on a simple strlen function2021-02-22T13:33:18Zmantis-gitlab-migrationE-ACSL: segmentation fault on a simple strlen functionID0002472:
**This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002472:
**This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002472 | Frama-C | Plug-in > E-ACSL | public | 2019-08-19 | 2019-08-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
E-ACSL successfully generates executable for this example and fails at runtime with segmentation fault error in shadow_alloca function at initialization stage.
<pre>
#include <stddef.h>
#include <stdint.h>
#include <stdio.h>
/*@ requires \exists size_t i; s[i] == '\0' && \valid_read(s+(0..i));
assigns \nothing;
ensures s[\result] == '\0';
ensures \forall size_t j; 0 <= j < \result ==> s[j] != '\0';
*/
size_t strlen(char *s)
{
size_t len;
/*@ loop invariant \forall size_t i; i < len ==> s[i] != '\0';
loop assigns len;
loop variant SIZE_MAX - len;
*/
for(len = 0; s[len] != '\0'; ++len);
return len;
}
int main(int argc, char *argv[])
{
for(int i = 0; i < argc; ++i) {
printf("%s: %d\n", argv[i], strlen(argv[i]));
}
return 0;
}
</pre>
### Additional Information :
$ gdb ./a.out.e-acsl
Temporary breakpoint 1, main (argc=1, argv=0x7fffffffd3e8) at a.out.frama.c:278
278 __e_acsl_memory_init(& argc,& argv,8UL);
Program received signal SIGSEGV, Segmentation fault.
shadow_alloca (ptr=ptr@entry=0x7fffffffd298, size=size@entry=8) at /home/work/.opam/framac/bin/../share/frama-c/e-acsl//segment_model/e_acsl_segment_tracking.h:562
562 prim_shadow[i] = (code << 2);
main function could be simple. For example, fails also in this case:
int main(void)
{
char *str = "0123456789";
printf("%s: %d\n", str, strlen(str));
return 0;
}
### Steps To Reproduce :
$ e-acsl-gcc.sh -c ./strlen.c
$ ./a.out.e-acsl
[1] 26340 segmentation fault (core dumped) ./a.out.e-acsl
## Attachments
- [strlen.c](/uploads/8cc47a4d07786ef1a83cc2d83a9ef725/strlen.c)https://git.frama-c.com/pub/frama-c/-/issues/136Crash at "hashtbl.ml", line 4622021-02-22T13:35:08Zmantis-gitlab-migrationCrash at "hashtbl.ml", line 462ID0002467:
**This issue was created automatically from Mantis Issue 2467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002467:
**This issue was created automatically from Mantis Issue 2467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002467 | Frama-C | Kernel | public | 2019-07-26 | 2019-08-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Victor Sverdlin | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | opensuse-tumbleweed | **OS Version** | 20190723 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Raised at file "hashtbl.ml", line 462, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
### Additional Information :
(* Frama-C journal generated at 16:46 the 26/07/2019 *)
exception Unreachable
exception Exception of string
[@@@ warning "-26"]
(* Run the user commands *)
let run () =
Project.set_keep_current false;
File.init_from_cmdline ();
Dynamic.Parameter.String.set ""
"/media/sf_home/temp/gps_try/sent_LDRA/src/main.c";
begin try
(* exception Log.AbortError("kernel") raised on: *)
File.init_from_cmdline ();
raise Unreachable
with
| Unreachable as exn -> raise exn
| exn (* Log.AbortError("kernel") *) ->
(* continuing: *)
begin try
(* exception Log.AbortError("kernel") raised on: *)
File.prepare_from_c_files ();
raise Unreachable
with
| Unreachable as exn -> raise exn
| exn (* Log.AbortError("kernel") *) ->
(* continuing: *) raise (Exception (Printexc.to_string exn))
end
end
(* Main *)
let main () =
Journal.keep_file "./.frama-c/frama_c_journal.ml";
try run ()
with
| Unreachable -> Kernel.fatal "Journal reaches an assumed dead code"
| Exception s -> Kernel.log "Journal re-raised the exception %S" s
| exn ->
Kernel.fatal
"Journal raised an unexpected exception: %s"
(Printexc.to_string exn)
(* Registering *)
let main : unit -> unit =
Dynamic.register
~plugin:"Frama_c_journal.ml"
"main"
(Datatype.func Datatype.unit Datatype.unit)
~journalize:false
main
(* Hooking *)
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
### Steps To Reproduce :
Just open new project and add at least one .c (or .h) file
## Attachments
- [main.c](/uploads/337a510fa380eff8f13edf74a7a7db10/main.c)https://git.frama-c.com/pub/frama-c/-/issues/84Can't build from source using opam2021-02-22T13:34:34Zmantis-gitlab-migrationCan't build from source using opamID0002466:
**This issue was created automatically from Mantis Issue 2466. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002466:
**This issue was created automatically from Mantis Issue 2466. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002466 | Frama-C | Opam | public | 2019-07-25 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sshankar | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | 18.04 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Argon doesn't build, presumably due to config related bugs in opam/opam. I am guessing its due to inconsistency with opam semantics of "|" (used under conflicts in $FRAMAC/opam/opam).
### Additional Information :
If possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks.
### Steps To Reproduce :
When I try to install it using the prescribed method
opam init
eval `opam config env`
opam install depext
opam depext frama-c
opam install --deps-only frama-c
cd ~/src (where argon is)
opam pin add --kind=path frama-c frama-c-18.0-Argon/
I get the following error (and no frama-c):
frama-c needs to be installed.
[ERROR] why3-base (< 0.88 | >= 1.0.0) & coq < 8.4.6 & lablgtk < 2.18.2 &
frama-c-e-acsl & frama-c-base is not a valid conjunction
[NOTE] Pinning command successful, but your installed packages may be out of
sync.https://git.frama-c.com/pub/frama-c/-/issues/121floating-point support is somwhat incomplete2021-02-22T12:56:27Zmantis-gitlab-migrationfloating-point support is somwhat incompleteID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002459 | Frama-C | Plug-in > wp | public | 2019-07-02 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | florian | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | any | **OS** | any | **OS Version** | any |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi!
Maybe I am doing something fundamentally wrong, but I've tried some simple programs and I don't get anywhere. For example:
/*@ requires x >= 0.0f && x <= 100.0f;
*/
void float_fun(float x)
{
float y = x + 1.0f;
//@ assert y >= 1.0f;
}
I've had a look in share/frama-c/wp/why3/Cfloat.why and I'm not surprised nothing works, the axiomatisation is very incomplete, compared to the current stuff in why3. Could you please port to https://gitlab.inria.fr/why3/why3/blob/master/stdlib/ieee_float.mlw and then use a SMT solver by default that supports it natively (i.e. CVC4 or Z3)?
I know this is a bit of a drastic change, but as it stands WP is not overly useful for anyone trying to do anything with floats (e.g. control systems)...https://git.frama-c.com/pub/frama-c/-/issues/179Can't use e-acsl on a dynamic library containing all the instrumentations2023-03-22T03:49:51Zmantis-gitlab-migrationCan't use e-acsl on a dynamic library containing all the instrumentationsID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002422:
**This issue was created automatically from Mantis Issue 2422. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002422 | Frama-C | Plug-in > E-ACSL | public | 2019-01-22 | 2019-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.19 Ocaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | - |
### Description :
Hi !
main.c contains the entry point : the main function and is not instrumented by frama-c
it calls instrumented func.c (e-acsl.func.c containing the __e_acsl_memory_init call) compiled as a dynamic library libe-acsl.func.so
then the e-acsl code segfault at
e_acsl_segment_tracking.h:815
### Additional Information :
Why the hell am I doing this ? :)
Contiki-NG is an IoT OS. It can be build as a firmware for several IoT devices, as a ELF for Linux x86/x86_64, and as a shared library loaded by the Java Cooja network simulator (with some JNI).
Before experimenting with dlopen in C and JNI in Java, which is going to fail because of the __executable_start symbol at ./share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h:47
(this will the subject of another future post)
I would like to be able, as a first step, to use a e-acsl instrumented dynamic library used by a non-instrumented program (containing main or not).
I am open to a solution that eventually needs some change inside the C E-ACSL code.
### Steps To Reproduce :
$ make
rm -vf *.*o ./loader ./main *e-acsl*
frama-c -main func -variadic-no-translation -machdep gcc_x86_64 -c11 -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64" -no-frama-c-stdlib func.c -e-acsl-prepare -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-full-mmodel -then-last -print -ocode e-acsl.func.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing func.c (with preprocessing)
[rte] annotating function __bswap_16
[rte] annotating function __bswap_32
[rte] annotating function __bswap_64
[rte] annotating function __uint16_identity
[rte] annotating function __uint32_identity
[rte] annotating function __uint64_identity
[rte] annotating function func
[e-acsl] beginning translation.
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap16, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap32, generating default assigns from the prototype
[kernel:annot:missing-spec] :0: Warning:
Neither code nor specification for function __builtin_bswap64, generating default assigns from the prototype
[kernel:annot:missing-spec] /usr/include/stdio.h:332: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
gcc -shared -fPIC -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_STACK_SIZE=32 -DE_ACSL_HEAP_SIZE=128 -std=c99 -m64 -O0 -g -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 -I/home/jean/local-frama-c/share/frama-c/e-acsl/ -o libe-acsl.func.so e-acsl.func.c /home/jean/local-frama-c/share/frama-c/e-acsl/e_acsl_rtl.c /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-dlmalloc.a /home/jean/local-frama-c/share/frama-c/../../lib/libeacsl-gmp.a -lm
gcc -o main main.c -L. -le-acsl.func
LD_LIBRARY_PATH=:./ ./main
Segmentation fault
make: *** [Makefile:11: e-acsl-main-shared] Error 139
## Attachments
- [e-acsl-is-fun.tar](/uploads/c1c5ac773627666455f1b0a93e66da53/e-acsl-is-fun.tar)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/58Wp crashes on a recursive function2021-02-22T13:34:36ZFrédéric LoulergueWp crashes on a recursive functionID0002420:
**This issue was created automatically from Mantis Issue 2420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002420:
**This issue was created automatically from Mantis Issue 2420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002420 | Frama-C | Plug-in > wp | public | 2018-12-28 | 2020-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | frederic.loulergue@nau.edu | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Mac | **OS** | macOS | **OS Version** | Mojave 10.14.1 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp tmp.c give the following trace. If the recursive call in e_get is removed, no crash.
[kernel] Parsing tmp.c (with preprocessing)
[wp] Running WP plugin...
[kernel] Current source was: tmp.c:14
The full backtrace is:
Raised by primitive operation at file "src/kernel_services/ast_data/statuses_by_call.ml", line 198, characters 11-65
Called from file "list.ml", line 82, characters 20-23
Called from file "src/kernel_services/ast_data/statuses_by_call.ml", line 231, characters 6-150
Called from file "src/plugins/wp/cil2cfg.ml", line 859, characters 6-35
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 1216, characters 13-47
Called from file "src/plugins/wp/cil2cfg.ml", line 1248, characters 6-30
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/wp/cil2cfg.ml" (inlined), line 1288, characters 13-33
Called from file "src/plugins/wp/wpAnnot.ml", line 1291, characters 12-26
Called from file "src/plugins/wp/wpAnnot.ml", line 1307, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1320, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 109, characters 4-67
Called from file "map.ml", line 291, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 137, characters 4-39
Called from file "src/plugins/wp/register.ml", line 686, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 332, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 332, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-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
Unexpected error (Stack overflow).
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
## Attachments
- [tmp.c](/uploads/db0023943b4d5bc953e110a335fcc7c7/tmp.c)https://git.frama-c.com/pub/frama-c/-/issues/180E-ACSL crash with RTE generated assertion with booleans2021-04-20T07:09:09Zmantis-gitlab-migrationE-ACSL crash with RTE generated assertion with booleansID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002412 | Frama-C | Plug-in > E-ACSL | public | 2018-12-03 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux x86_64 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
There might be a regression with the RTE or E-ACSL plugin with Argon.
/////////// boolean.c
#include <stdbool.h>
bool return_false(void)
{
return false;
}
int main(void)
{
return 0;
}
///////////////////////////
### Additional Information :
On Chlorine-20180502 (bfd93b819) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
### Steps To Reproduce :
On Argon 18.0 (2f7a0eee0) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Current source was: rte_boolean.c:10
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
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
Unexpected error (Stack overflow).
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
## Attachments
- [boolean.c](/uploads/1b34c066b4dc860013dcc10c38a49aad/boolean.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/116crash2021-02-22T12:54:02Zmantis-gitlab-migrationcrashID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002409 | Frama-C | Plug-in > wp | public | 2018-11-13 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | macosx | **OS** | mojave | **OS Version** | 10.14.1 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp somme.c
with somme.c containing
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
leads to crash
Trace below
### Additional Information :
[kernel] Parsing somme.c (with preprocessing)
[wp] Failure: Unbound logic variable 'f'
[kernel] Current source was: somme.c:4
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16
Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38
Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "list.ml", line 88, characters 20-23
Called from file "list.ml", line 88, characters 32-39
Called from file "list.ml", line 88, characters 32-39
Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51
Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60
Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104
Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46
Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42
Called from file "map.ml", line 295, characters 20-25
Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47
Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45
Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36
Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 19-28
Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36
Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023
Called from file "src/plugins/wp/register.ml", line 689, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-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 791, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Chlorine-20180502.
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
hugo-9:TP3 gimbert$ cat somme.c
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
## Attachments
- [somme.c](/uploads/5ef73e24f859da4da063d6d4e135ea99/somme.c)https://git.frama-c.com/pub/frama-c/-/issues/240frama-clang fails to compile2022-09-28T11:04:53Zmantis-gitlab-migrationframa-clang fails to compileID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002402:
**This issue was created automatically from Mantis Issue 2402. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002402 | Frama-C | Plug-in > clang | public | 2018-10-01 | 2018-10-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | barafael | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to compile frama-clang, I encounter
Error: Unbounded constructor ASinteger
in file convert_acsl.ml.
ASidentifier is also missing.
### Steps To Reproduce :
Get sources for frama-clang-0.0.6, configure, makeVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/75Failure to detect qed libraries when running wp2021-02-22T12:52:46Zmantis-gitlab-migrationFailure to detect qed libraries when running wpID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002389 | Frama-C | Plug-in > wp | public | 2018-07-17 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 17-Chlorine | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
This is not a problem with this particular code, but I will include it anyways for the sake of completeness and reproducibility.
With the following C code "average.c"
=============================================
/*@ ensures \result == \abs(x); */
double abs(double x) {
if (x >= 0) return x;
else return (-x);
}
/*@ requires 0x1p-967 <= C <= 0x1p970;
@ ensures \result == \round_double(\NearestEven, (x+y)/2);
@ */
double average(double C, double x, double y) {
if (C <= abs(x)) return x/2+y/2;
else return (x+y)/2;
}
=============================================
running the command
>frama-c -wp -wp-model +float -wp-prover "why3:coq" -wp-print average.c
produces the following output
=============================================
[kernel] Parsing average.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] average.c:9: Warning:
Builtin \NearestEven not defined
[wp] 2 goals scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
... (less relevant output) ...
=============================================
the line referenced in coq.drv is
"theory qed.Qed meta "realized_theory" "qed.Qed", "Qed" end
### Additional Information :
Product Version: Frama-C-Chlorine-20180501 **not an option in reporting tool**
I reported this here because the error seems to be with the configurations files generated by frama-c in the frama-c/wp directory, but I can't be sure that the problem isn't with why3 itself. I'm still very new to using these tools.
Note: the "Builtin \NearestEven not defined" seems to be a separate bug, referenced here: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-July/005117.html
### Steps To Reproduce :
Installed the following via OPAM
coq 8.8.0 (because 8.8.1+ reports not supported by why3)
why3-coq 1.0.0
frama-c-chlorine-20180501
error persists after uninstalling and re-installing all of the above
## Attachments
- [coq.drv](/uploads/7d46c6d1e6ee9a9a0ee6e60e0dbb72f7/coq.drv)
- [wp.driver](/uploads/9801629381f7c222b5f698622a1d6551/wp.driver)https://git.frama-c.com/pub/frama-c/-/issues/113Auto-generated assigns clause for a void* argument crashes wp2021-02-22T13:34:40Zmantis-gitlab-migrationAuto-generated assigns clause for a void* argument crashes wpID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | schollet | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
### Additional Information :
The command run :
frama-c -wp test2.c
Error log :
[kernel] Parsing test2.c (with preprocessing)
[kernel:annot:missing-spec] test2.c:7: Warning:
Neither code nor specification for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] test2.c:11: User Error: Invalid infinite range i_0+(0..)
[kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui):
/*@ assigns *((char *)thing + (0 ..));
assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..));
*/
Removing the assigns clause for create stops WP from crashing
### Steps To Reproduce :
run `frama-c -wp test2.c` with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause.
Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file
## Attachments
- [assigns.tar.gz](/uploads/7d8c7280dce8dde42f8cce1f86cbef35/assigns.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/263frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined size...2021-04-20T17:20:20Zmantis-gitlab-migrationframa-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002376:
**This issue was created automatically from Mantis Issue 2376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002376 | Frama-C | Plug-in > jessie | public | 2018-05-29 | 2018-05-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | foo | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi all,
I'm very new to the frama-c and why ecosystem. I hope it's really a bug with frama-c and not jessie.
The C input is:
#include<stdlib.h>
int main(void) {
char *p =malloc(5);
p[0] = 4;
return 3;
}
I'd like to verify that the write to p[0] goes toa valid address.
$ Frama-c -val -jessie t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_random_counter ∈ [--..--]
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_mblen_state ∈ [--..--]
__fc_mbtowc_state ∈ [--..--]
__fc_wctomb_state ∈ [--..--]
t.c:4:[value] allocating variable __malloc_main_l4
t.c:5:[value] warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
p ∈ {{ &__malloc_main_l4[0] }}
__retres ∈ {3}
__malloc_main_l4[0] ∈ {4}
[1..4] ∈ UNINITIALIZED
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:389
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 5238, characters 9-67
Called from file "common.ml", line 329, characters 27-46
Called from file "norm.ml", line 1551, characters 11-55
Called from file "norm.ml", line 1571, characters 37-71
Called from file "norm.ml", line 1614, characters 22-47
Called from file "norm.ml", line 1685, characters 19-43
Called from file "src/kernel_services/ast_queries/cil.ml", line 2239, characters 15-31
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 3543, characters 17-35
Called from file "src/kernel_services/ast_queries/cil.ml", line 3572, characters 12-19
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 3576, characters 23-50
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3613, characters 14-38
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 3602, characters 5-80
Called from file "src/kernel_services/ast_queries/cil.ml", line 3840, characters 16-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 2278, characters 13-16
Called from file "src/kernel_services/ast_queries/cil.ml", line 2323, characters 24-57
Called from file "src/kernel_services/ast_queries/cil.ml", line 3808, characters 5-53
Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 6463, characters 17-37
Called from file "src/kernel_services/ast_queries/cil.ml", line 6468, characters 24-33
Called from file "src/kernel_services/ast_queries/cil.ml", line 6470, characters 3-20
Called from file "src/kernel_services/ast_queries/cil.ml", line 2254, characters 21-41
Called from file "src/kernel_services/ast_queries/cil.ml", line 6487, characters 15-39
Called from file "common.ml", line 580, characters 2-13
Called from file "norm.ml", line 1959, characters 2-26
Called from file "register.ml", line 158, characters 4-23
Called from file "register.ml", line 278, characters 6-12
Called from file "src/kernel_services/plugin_entry_points/journal.ml", line 442, characters 19-22
Re-raised at file "src/kernel_services/plugin_entry_points/journal.ml", line 457, characters 10-17
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sulfur-20171101.
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
[kernel] writing journal in file `./.frama-c/frama_c_journal.ml'.
### Additional Information :
I'm using
frama-c Sulfur-20171101
why 2.40
Why3 0.88.3
ocaml 4.06.1
## Attachments
- [frama_c_journal.ml](/uploads/d55e08324ce8dc26fa7317cab9a5d1be/frama_c_journal.ml)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/262Strange difference in generated Coq code between Chlorine and Sulfur2021-02-22T13:37:10ZJens GerlachStrange difference in generated Coq code between Chlorine and SulfurID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002374 | Frama-C | Plug-in > wp | public | 2018-05-09 | 2018-06-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This report refers to the BETA-release of Chlorine and affects a couple of Coq-proofs in ACSL by Example:
The problem is like this: If the attached file 'foo.c' is processed with the command line
frama-c -wp -wp-prover coq -wp-out foo.wp foo.c
then it produces in foo.wp among other files the Coq file A_Count.v.
The only difference when using with Frama-C-Sulfur or Frama-C-Chlorine is the following:
diff A_Count.sulfur.v A_Count.chlorine.v
28,32c28,32
< Hypothesis Q_CountSectionHit: 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) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
< (((1 + ((L_Count t a i%Z x i_2%Z))) = ((L_Count t a i%Z i_1%Z i_2%Z)))%Z).
---
> Hypothesis Q_CountSectionHit: 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 ((i < i_1)%Z) ->
> ((is_sint32 x_1)) ->
> (((1 + ((L_Count t a i%Z x x_1))) = ((L_Count t a i%Z i_1%Z x_1)))%Z).
It looks like as if the argument 'v' of axiom 'CountSectionHit' has not been translated into Coq.
## Attachments
- [foo.c](/uploads/53423ef104c4f86e7469ef5bb783ec52/foo.c)
- [A_Count.sulfur.v](/uploads/774888275fb8101cef0293aaee7dafa5/A_Count.sulfur.v)
- [A_Count.chlorine.v](/uploads/878201905680422222e1b2e12a40293d/A_Count.chlorine.v)https://git.frama-c.com/pub/frama-c/-/issues/256Crash on attempt to start framaCIRGen when libs are linked statically and dyn...2021-02-22T12:57:36Zmantis-gitlab-migrationCrash on attempt to start framaCIRGen when libs are linked statically and dynamically.ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002368 | Frama-C | Plug-in > clang | public | 2018-02-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DeMaze | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | GNU/Linux | **OS** | Debian | **OS Version** | 9.3 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
On the attempt to install Frama-Clang regularly as described (see
attached file installation.txt), the executable framaCIRGen exits with
an error when executed. The error message points to a problem with
LLVM. In fact, it depicts one commandline option to be registered more
than once. This occurs on the attempt of using Frama-C to parse C++
source code and when the executable framaCIRGen is invoked manually on
the commandline. I get the following error:
<output nr="0" command="./frama-clang-0.0.4/bin/framaCIRGen">
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
</output>
However, this has only been observed ith llvm-5.0 on Debian GNU/Linux
9.3 (my system, see lsb_release_3ffbf_2018-02-10000905) for now. With
llvm 3.9, no such errors happen. Presumably, versions of llvm > 5.0
could also be affected. This seems to be a problem many people have
experienced with llvm related programs [2][3][4][5]. In fact, it has
even been reported for frama-clang [6].
### Additional Information :
Root Cause
==========
As far as my investigations revealed, this problem occurs because of
the linking mechanism on Debian GNU/Linux. On this distribution,
libraries of LLVM are built two-fold:
Static archives (lib*.a):
clangFrontend, clangDriver, clangTooling, clanParse, clangSema,
clangAnalysis, clangEdit, clangAST, clangLex, clangSerialization,
clangBasic, LLVMTransformUtils, LLVMBitReader, LLVMMCParser,
LLVMOption
Shared object (lib*.so):
LLVM-5.0
Therefore, it is tried to link them according to their type (lines 74-77, 82-85):
<output nr="1" command="cat frama-clang-0.0.4/Makefile.clang -n | grep 'USEDLIBS' -A 5 -B 5 ">
69 CFLAGS+=-g
70 CLANG_LINKFLAGS+=-g
71 endif
72
73 #LINK_COMPONENTS := $(TARGETS_TO_BUILD) asmparser support mc
74 USEDLIBS = clangFrontend \
75 clangDriver clangTooling clangParse clangSema \
76 clangAnalysis clangEdit clangAST clangLex clangSerialization \
77 clangBasic LLVMTransformUtils LLVMBitReader LLVMMCParser LLVMOption
78
79 # for use in main Makefile
80 default: $(PLUGIN_DIR)/bin/$(TOOLNAME)
81
82 $(PLUGIN_DIR)/bin/$(TOOLNAME): $(OBJS) $(PLUGIN_DIR)/bin
83 $(PRINT_LINKING) $@
84 $(CXX) $(CLANG_LINKFLAGS) -o $@ \
85 $(OBJS) $(addprefix -l,$(USEDLIBS)) $(LLVM_LIBS) $(CLANG_SYSLIBS) $(CLANG_LINKFLAGS)
86
87 $(PLUGIN_DIR)/bin:
88 $(MKDIR) $@
89
90 clean:
</output>
This results in the following dependencies on dynamic libraries as follows:
<output n="2" command="ldd ./frama-clang-0.0.4/bin/framaCIRGen">
linux-vdso.so.1 (0x00007ffe31ff5000)
libLLVM-5.0.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-5.0.so.1 (0x00007fb4c4825000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb4c44a3000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb4c419f000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb4c3f88000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb4c3be9000)
libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007fb4c39e0000)
libedit.so.2 => /usr/lib/x86_64-linux-gnu/libedit.so.2 (0x00007fb4c37a8000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fb4c35a0000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb4c339c000)
libtinfo.so.5 => /lib/x86_64-linux-gnu/libtinfo.so.5 (0x00007fb4c3172000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb4c2f55000)
libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007fb4c2d3b000)
/lib64/ld-linux-x86-64.so.2 (0x00007fb4c9431000)
libncurses.so.5 => /lib/x86_64-linux-gnu/libncurses.so.5 (0x00007fb4c2b18000)
libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x00007fb4c2902000)
</output>
From this output, this assumption can be confirmed because
ligcc_s.so.1 as well as libLLVM-5.0.so.1 occurs. A response on a bug
report of LLVM considers this as rather bad practice
however. Moreover, this is mentioned as a classical problem of LLVM's
"global object-based commandline switch registration" [1]:
"The command line option error is the classical problem one gets due
to the LLVM's global object-based command line switch registration. If
you somehow link the same global object (that registers the command
line option) twice via dynamic loading of the LLVM library twice or
more to the same process, it registers the same command line object
again (when calling the global object initializer), resulting in this
error." [1]
The aforementioned symbol 'asm-macro-max-nesting-depth' occurs both in
libLLVMMCParser.a and libLLVM-5.0.so.1 . Hence, I conjecture these are
the files in conflict.
My Solution
===========
Just link without libLLVMMCParser.a or more precisely, remove
LLVMMCParser from USEDLIBS in Makefile.clang. This seems to work as
C++ code is analyzable again. Please find patches for Makefile.clang
attached which circumvent this problem according to my proposal
(Makefile.clang.patch / Makefile.clang.patch.better). Feel free to
contacting me in case of any further quesions / comments.
References
==========
[1] https://bugs.llvm.org/show_bug.cgi?id=30587#c6
[2] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=768185
[3] https://bugs.llvm.org/show_bug.cgi?id=31571
[4] http://llvm.1065342.n5.nabble.com/llvm-dev-LLD-and-LLVM-LINK-LLVM-DYLIB-td104570.html
[5] https://github.com/zig-lang/zig/issues/67
[6] https://stackoverflow.com/questions/45647503/errors-when-using-the-frama-clang-plugin
### Steps To Reproduce :
1. Manually install llvm-5.0 as described on https://apt.llvm.org/
2. Download and build frama-clang as described officially with llvm-5.0
3. Execute ./bin/framaCIRGen
## Attachments
- [logs_and_more.tar.xz](/uploads/d2a4d0490b88cd4c21961e8a55ab0ca2/logs_and_more.tar.xz)https://git.frama-c.com/pub/frama-c/-/issues/274"Here" as predicate label in statement contract causes Segmentation fault2021-02-22T12:58:03ZJochen Burghardt"Here" as predicate label in statement contract causes Segmentation faultID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002360 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp rotate_cpp.cpp" on the attached program outputs an error message "rotate_cpp.cpp:5:23: expecting a label argument", and then crashes due to a Segmentation fault. The problem disappears when the statement contract in line 5 is changed into an assertion.
## Attachments
- [rotate_cpp.cpp](/uploads/56cddcc4aad61f74882ab6f0a55106cf/rotate_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/273"assigns" in statement contract causes abort or crash2021-02-22T12:58:03ZJochen Burghardt"assigns" in statement contract causes abort or crashID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002361 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c remove_cpp.cpp" on the attached program outputs
"framaCIRGen: ACSLStatementAnnotation.cpp:248: Parser::Base::ReadResult Acsl::StatementAnnotation::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed."
and then aborts. If the "ensures" clause in line 5 is removed, Frama-C outputs instead:
"*** Error in `framaCIRGen': double free or corruption (out): 0x0000559f983d0160 ***"
and then aborts, too. If in addition "a[0..9]" is removed from the "assigns" claus in line 4, Frama-C crashes (Segmentation fault) without printing any error message before. For the latter reason, I've set the severity to "crash".
## Attachments
- [remove_cpp.cpp](/uploads/2af0af96279845d9332c5293876e6c3e/remove_cpp.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/281Frama-Clang crashes on error in contract2021-02-22T13:36:01ZJens GerlachFrama-Clang crashes on error in contractID0002352:
**This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002352:
**This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002352 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached example uses mistakenly the assignment operator = instead of == in the ensures clause.
Frama-Clang crashes on this example.
frama-c -wp -wp-rte assignment_in_contract.cpp
[kernel] Parsing assignment_in_contract.cpp (external front-end)
framaCIRGen: ACSLTermOrPredicate.cpp:7096: Parser::Base::ReadResult Acsl::TermOrPredicate::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "assignment_in_contract.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
A message along the lines of normal Frama-C
"user error: Assignment operators not allowed in annotations."
would be more helpful.
## Attachments
- [assignment_in_contract.cpp](/uploads/f0d2dd6918d688ca68e2c4996617c929/assignment_in_contract.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/286direct initialisation of bool by nullptr2021-02-22T13:36:06ZJens Gerlachdirect initialisation of bool by nullptrID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002347 | Frama-C | Plug-in > clang | public | 2018-01-22 | 2018-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached program "nullptr_crash.cpp" compiles without warnings with g++-7.2 in C++11 mode.
Clang-5.0 issues a warning (and if I understood the standard correctly, it shouldn't, because the example uses "direct initialisation").
Frama-Clang crashes on the example.
The second example "nullptr_bool.cpp" which uses "copy initialisation" only warns about implicit conversion...
## Attachments
- [nullptr_crash.cpp](/uploads/7975ccda4df20b073580f91557d4e559/nullptr_crash.cpp)
- [nullptr_bool.cpp](/uploads/cecfd360ef834b1bcbf7a7a9606df04f/nullptr_bool.cpp)
- [nullptr_no_crash.cpp](/uploads/7bfd118ea401a367676355d8352849c2/nullptr_no_crash.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/254Crash when trying to analyse a file with jessie2021-04-15T09:16:54Zmantis-gitlab-migrationCrash when trying to analyse a file with jessieID0002334:
**This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002334:
**This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002334 | Frama-C | Plug-in > jessie | public | 2017-12-06 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | 4.7.9 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
When running "frama-c -jessie jessie-crash.c" on the attached file, I get the following crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing encoding.c (with preprocessing)
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_string_axiomatic.h:35
The full backtrace is:
Raised at file "interp.ml", line 2383, characters 5-24
Called from file "interp.ml", line 2644, characters 22-41
Called from file "list.ml", line 70, characters 22-25
Called from file "interp.ml", line 2731, characters 27-66
Called from file "register.ml", line 175, characters 16-32
Called from file "register.ml", line 278, characters 6-12
Re-raised at file "register.ml", line 251, characters 29-103
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (File "interp.ml", line 2383, characters 5-11: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501.
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
My packages are at the following version:
frama-c 20170501
why 2.39
why3 0.87.3
ocaml 4.03.0
## Attachments
- [jessie-crash.c](/uploads/d0c7ce11aeaa47a5db5fcf2126955551/jessie-crash.c)