frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-03-30T08:44:29Z
https://git.frama-c.com/pub/frama-c/-/issues/250
cast error with reference fields
2021-03-30T08:44:29Z
mantis-gitlab-migration
cast error with reference fields
ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002396 | Frama-C | Plug-in > clang | public | 2018-08-24 | 2018-08-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abhishek.anand.iitg@gmail.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | manjaro | **OS Version** | 8/23/3018 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
```
class B {
};
template <typename T>
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
B b;
B & y=b;
A<B> a(y);
}
```
I get the following error:
```
root@27db7a69b96a:/hostshare# frama-c -print refFieldBug.cpp
[kernel] Parsing refFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] refFieldBug.cpp:8: Failure: castTo struct _Z1B -> struct _Z1B *
[kernel] User Error: stopping on file "refFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user inp
```
I don't see what could be the problem because the following succeeds:
```
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
int x=0;
int & y=x;
A<int> a(y);
}
```
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/76
conditional input annotations result in why3 type errors
2021-02-22T12:52:48Z
mantis-gitlab-migration
conditional input annotations result in why3 type errors
ID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002394 | Frama-C | Plug-in > wp | public | 2018-08-23 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | GNU/Linux | **OS Version** | Debian 9 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I am trying to put conditions on my function specification that specify return values conditioned on special input values. A minimal example is as follows:
/*@ requires 0 <= t <= 1;
@ ensures t == 1.f ==> \result == b;
@ assigns \nothing
*/
float interpolate(float a, float b, float t) { ... }
Why3 (stderr) reports:
===================================================================================
File "/tmp/wp0a3ed9.dir/typed/interpolate_Why3_ide.why", line 20, characters 11-26:
This term has type real -> real, but is expected to have type real
===================================================================================
The "problem line" is "ensures t == 1.f ==> \result == b;"
This seems to be a problem between wp and why3. The error persists with every external prover I use with why3. The list of provers I've tried is [Z3,CVC3,CVC4,Alt-Ergo,Gappa], and the only exception is why3:coq (see issue 0002389).
### Additional Information :
why3 0.88.3
frama-c chlorine 20180502
### Steps To Reproduce :
see attached file "buggy.c"
run:
> frama-c -wp -wp-prover "why3:XXX" buggy.c
where XXX is any prover installed with why3
## Attachments
- [buggy.c](/uploads/323bd028ec39d43d549eae1d88957797/buggy.c)
https://git.frama-c.com/pub/frama-c/-/issues/248
Frama-C GUI manual
2021-02-22T12:57:24Z
mantis-gitlab-migration
Frama-C GUI manual
ID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002393:
**This issue was created automatically from Mantis Issue 2393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002393 | Frama-C | Documentation > manuals | public | 2018-08-09 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Is there any detailed (stepwise) manual about GUI of Drama-C?
May be I'm missing some points but Could we edit/write new files within GUI interface? GUI seems to be not very user friendly...
https://git.frama-c.com/pub/frama-c/-/issues/251
request of clarification about using the address of a formal argument
2021-02-22T13:48:48Z
Jens Gerlach
request of clarification about using the address of a formal argument
ID0002392:
**This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002392:
**This issue was created automatically from Mantis Issue 2392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002392 | Frama-C | Documentation > ACSL | public | 2018-07-25 | 2018-07-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
In #2390 the issue was raised whether functions contracts such as
/*@ requires
\valid(&a);
ensures \false; */
void f(int a) {
return ;
}
are meaningful.
More specifically, the ACSL manual should clarify whether using the address of a formal argument in a precondition is illegal.
(When I see that WP uses such a precondition to verify \false, them I am all in for disallowing it.)
Of course, it would also be nice if Frama-C (the kernel?) would issue a diagnostics.
### Additional Information :
The question also came up about using the address of a formal argument in a postcondition.
For the time being, I don't see it as a meaningful feature.
https://git.frama-c.com/pub/frama-c/-/issues/247
Can't compile
2021-02-22T13:35:44Z
mantis-gitlab-migration
Can't compile
ID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002391 | Frama-C | Kernel > Makefile | public | 2018-07-25 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yurichev | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x64 | **OS** | Ubuntu Linux | **OS Version** | 16.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Got this file: https://frama-c.com/download/frama-c-Chlorine-20180502.tar.gz
Unpacked, typed "./configure", then "make" and got:
======================================================================
...
Ocamlc src/libraries/datatype/type.cmi
Ocamlc src/kernel_services/plugin_entry_points/log.cmi
Ocamlc src/libraries/project/project_skeleton.cmi
Ocamlc src/libraries/utils/pretty_utils.cmi
Ocamlc src/libraries/stdlib/integer.cmi
File "src/libraries/stdlib/integer.mli", line 26, characters 9-12:
Error: Unbound module Z
share/Makefile.generic:70: recipe for target 'src/libraries/stdlib/integer.cmi' failed
make: *** [src/libraries/stdlib/integer.cmi] Error 2
======================================================================
## Attachments
- [make_stdout](/uploads/401d9f44f320b484e178a6155274ee0d/make_stdout)
- [make_stderr](/uploads/8ecf375aceb48adc242fde2b25e103a0/make_stderr)
- [config.log](/uploads/cd25941939119614209fbc318815d10f/config.log)
https://git.frama-c.com/pub/frama-c/-/issues/115
dubious discharge of postcondition
2021-02-22T14:00:51Z
Jens Gerlach
dubious discharge of postcondition
ID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following function
/*@
assigns \nothing;
ensures a == 0;
*/
void foo(int a)
{
a = 0;
}
The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state.
If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here
/*@
requires \valid(&a);
assigns \nothing;
ensures a == 0;
*/
void bar(int a)
{
a = 0;
}
then Qed discharges the postcondition.
I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition
but in any case it would be nice if someone could have a look at it.
### Steps To Reproduce :
Call
frama-c -wp -wp-rte foo.c
on the attached file.
## Attachments
- [foo.c](/uploads/59eb64f1e1b8ca2563cbfa0bcbb63a83/foo.c)
https://git.frama-c.com/pub/frama-c/-/issues/75
Failure to detect qed libraries when running wp
2021-02-22T12:52:46Z
mantis-gitlab-migration
Failure to detect qed libraries when running wp
ID0002389:
**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/246
WP is not able to validate a statically declared structure followed by a memset
2021-02-22T12:57:18Z
Patricia Mouy
WP is not able to validate a statically declared structure followed by a memset
ID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002387 | Frama-C | Plug-in > wp | public | 2018-07-11 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
By using a clean way to declare the structure, WP fails to validate the structure but by using a "dirty" way, it works !
#include <string.h>
typedef struct {
int i;
float f;
} stest;
void notclean_but_valid() {
char b[sizeof(stest)];
stest *s = b;
memset(s, 0, sizeof(stest));
}
void clean_but_invalid() {
stest s;
memset(&s, 0, sizeof(stest));
}
### Steps To Reproduce :
frama-c -wp-model typed_cast_ref -wp struc.c
https://git.frama-c.com/pub/frama-c/-/issues/234
E-ACSL: internal error: raised at file "src/libraries/project/project.ml", li...
2021-02-22T12:57:00Z
mantis-gitlab-migration
E-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402
ID0002386:
**This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002386:
**This issue was created automatically from Mantis Issue 2386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002386 | Frama-C | Plug-in > E-ACSL | public | 2018-07-06 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | fmaurica | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 18-Argon | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Error:
<pre>
$ frama-с -version
Chlorine-20180501
$ frama-с -e-acsl memchr.c
...
[e-acsl] test.c:21: Warning:
E-ACSL construct `variant' is not yet supported. Ignoring annotation.
[e-acsl] test.c:27: Warning:
invalid E-ACSL construct
`non integer variable k in quantification ∀ u8 *k; (u8 *)s ≤ k < p ⇒ *k ≢ (u8)c'.
Ignoring annotation.
[kernel] test.c:26: Failure:
mkBinOp: p - (unsigned char const *)s == __gen_e_acsl_at - n
[kernel] Current source was: test.c:39
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 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
Frama-C aborted: internal error.
</pre>
Example code:
<pre>
/*@ requires \typeof(s) <: \type(u8 *);
requires \valid((u8 *)s+(0..n-1));
assigns \nothing;
behavior found:
assumes \exists u8 *p; (u8 *)s <= p < (u8 *)s + n && *p == (u8) c;
ensures s <= \result <= s + n;
ensures \forall u8 *p; (u8 *)s <= p < (u8 *)\result ==> *p != (u8) c;
ensures *((u8 *)\result) == (u8) c;
behavior not_exists:
assumes \forall u8 *p; (u8 *)s <= p < (u8 *)s + n ==> *p != (u8) c;
ensures \result == \null;
complete behaviors;
disjoint behaviors;
*/
void *memchr(const void *s, int c, size_t n)
{
const unsigned char *p = s;
/*@ loop invariant 0 <= n <= \at(n,Pre);
loop invariant (u8 *)s <= p <= (u8 *)s + \at(n,Pre);
loop invariant p - s == \at(n,Pre) - n;
loop invariant \forall u8 *k; (u8 *)s <= k < p ==> *k != (u8) c;
loop variant n;
*/
while (n-- != 0) {
if ((unsigned char) c == *p++) {
return (void *)(p - 1);
}
}
//@ assert n == (size_t)(-1);
return NULL;
}
int main(int argc, char *argv[])
{
const char *s = "1234567890";
void *ptr;
ptr = memchr(s, '0', 11);
ptr = memchr(s, 'a', 11);
ptr = ptr;
return 0;
}
</pre>
## Attachments
- [memchr.c](/uploads/6c87db6bb9861d6b6bb7f2ceb372297c/memchr.c)
- [memchr_v2.c](/uploads/d8f9701b3619dadb6d3936ef60d08be8/memchr_v2.c)
https://git.frama-c.com/pub/frama-c/-/issues/113
Auto-generated assigns clause for a void* argument crashes wp
2021-02-22T13:34:40Z
mantis-gitlab-migration
Auto-generated assigns clause for a void* argument crashes wp
ID0002385:
**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/261
WP: internal error: only the kernel should set the status of property assumes
2021-02-22T12:57:46Z
mantis-gitlab-migration
WP: internal error: only the kernel should set the status of property assumes
ID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002383 | Frama-C | Plug-in > wp | public | 2018-07-04 | 2018-07-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Example:
<pre>
int test(void)
{
int a = 1;
/*@ behavior ok:
assumes a > 0;
ensures \true;
*/
return 3;
}
</pre>
Command:
<pre>
frama-c -wp test.c
</pre>
Log:
<pre>
[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable)
[wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable)
[kernel] failure: only the kernel should set the status of property assumes
a > 0
[kernel] Current source was: test.c:1
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16
Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109
Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80
Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71
Called from file "list.ml", line 85, characters 12-15
Called from file "list.ml", line 85, characters 12-15
Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38
Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67
Called from file "map.ml", line 270, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
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
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
</pre>
## Attachments
- [test.c](/uploads/2597c1f73c5b7b83511f003173086460/test.c)
https://git.frama-c.com/pub/frama-c/-/issues/228
user error: scalar value (of type int) initialized by compound initializer
2021-02-22T12:56:50Z
mantis-gitlab-migration
user error: scalar value (of type int) initialized by compound initializer
ID0002384:
**This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002384:
**This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002384 | Frama-C | Kernel | public | 2018-07-04 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Example:
<pre>
struct test {
union {
int a;
long b;
};
};
static struct test t = { { .a = 0 } };
</pre>
Run:
<pre>
$ gcc -c test.c
$ echo $?
0
$ frama-c test.c
</pre>
Error Log:
<pre>
[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:1: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[kernel] test.c:8: User Error:
scalar value (of type int) initialized by compound initializer
6 };
7
8 static struct test t = { { .a = 0 } };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[kernel] User Error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
</pre>
Frama-C Version:
<pre>
$ frama-c -version
Chlorine-20180501
</pre>
## Attachments
- [test.c](/uploads/9b2870c999eda7e90e97626672511315/test.c)
- [restore-initializers.patch](/uploads/9236fdb360274563d8f5bbc41595bd8c/restore-initializers.patch)
https://git.frama-c.com/pub/frama-c/-/issues/154
handling of escape sequences
2021-02-22T13:40:11Z
mantis-gitlab-migration
handling of escape sequences
ID0002382:
**This issue was created automatically from Mantis Issue 2382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002382:
**This issue was created automatically from Mantis Issue 2382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002382 | Frama-C | Kernel | public | 2018-07-03 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
Code:
<pre>
/*@
predicate isspace(integer c) = c == ' ' || c == '\f' || c == '\n' ||
c == '\r' || c == '\t' || c == '\v';
*/
</pre>
Error:
<pre>
[kernel] Parsing test.h (with preprocessing)
test.h:2:[kernel] failure: Unknown error (File "src/kernel_internals/parsing/logic_lexer.mll", line 390, characters 20-26: Assertion failed)
</pre>
Need to support '\v'.
## Attachments
- [escape_sequences.c](/uploads/24f837eb87b6ff67601f79146e0f08eb/escape_sequences.c)
https://git.frama-c.com/pub/frama-c/-/issues/252
E-ACSL: vla handling
2021-02-22T14:01:19Z
mantis-gitlab-migration
E-ACSL: vla handling
ID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002381:
**This issue was created automatically from Mantis Issue 2381. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002381 | Frama-C | Plug-in > E-ACSL | public | 2018-07-01 | 2018-07-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code:
<pre>
int main(void)
{
int size = 10;
int array[size];
return 0;
}
</pre>
<pre>
a.out.frama.c:141: undefined reference to `__fc_vla_alloc'
a.out.frama.c:143: undefined reference to `__fc_vla_free'
collect2: error: ld returned 1 exit status
e-acsl-gcc: fatal error: fail to compile/link instrumented code
</pre>
https://git.frama-c.com/pub/frama-c/-/issues/224
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.
2021-02-22T12:56:40Z
mantis-gitlab-migration
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.
ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002380 | Frama-C | Plug-in > wp | public | 2018-06-23 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | namin | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
`strlen` used from code makes it no longer possible to prove `assigns \nothing`. The definition in the Frama-C library has `@ assigns \result \from indirect:s[0..];`, but this should not prevent check?
### Steps To Reproduce :
$ cat bug.c
#include <string.h>
/*@
requires strlen(s)>=0 && \valid(s+(0..strlen(s)));
assigns \nothing;
*/
int len(char *s) {
return strlen(s);
}
$ frama-c -wp -wp-rte -wp-prover CVC4,alt-ergo bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function len
[wp] 5 goals scheduled
[wp] [Failed] Goal typed_len_assign_normal_part1
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (324ms)
[wp] [Failed] Goal typed_len_assign_exit
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (322ms)
[wp] Proved goals: 3 / 5
Qed: 2 (0.35ms-0.85ms-2ms)
Alt-Ergo: 1 (15ms) (20) (unknown: 2)
CVC4: 0 (interrupted: 2)
https://git.frama-c.com/pub/frama-c/-/issues/229
FE_* API is available on OpenBSD
2021-02-22T12:56:52Z
mantis-gitlab-migration
FE_* API is available on OpenBSD
ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002379:
**This issue was created automatically from Mantis Issue 2379. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002379 | Frama-C | Kernel > libc | public | 2018-06-18 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | any | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
please include attached patch.
## Attachments
- [patch-src_libraries_utils_c_bindings_c](/uploads/5d11f5d41c049aab5269993f94365e40/patch-src_libraries_utils_c_bindings_c)
https://git.frama-c.com/pub/frama-c/-/issues/73
Bytecode only compilation fails when linking to stdlib
2021-02-22T12:52:37Z
mantis-gitlab-migration
Bytecode only compilation fails when linking to stdlib
ID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002378 | Frama-C | ptests | public | 2018-06-18 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | bytecode-only | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Compiling bytecode only fails with this error:
ocamlfind ocamlc -I ptests -dtypes -vmthread -g -o bin/ptests.byte unix.cma threads.cma str.cma dynlink.cma ptests/ptests_config.ml ptests/ptests.ml
File "ptests/ptests.ml", line 1:
Error: Required module `Uchar' is unavailable
### Steps To Reproduce :
Compile OCaml >=4.03 without optimizing compilers.
Use this compiler to build frama-c
## Attachments
- [patch-configure_in](/uploads/bf282dbc3c08065b0ff2a13f4fb83464/patch-configure_in)
- [patch-Makefile](/uploads/8465ce62432109e8765f692552e038a5/patch-Makefile)
- [patch-configure_in_2](/uploads/0fc49374e72889fac876d95a3de5dd71/patch-configure_in_2)
- [patch-Makefile_2](/uploads/568208604221bf782f915ed5f2ccf1b0/patch-Makefile_2)
- [patch-Makefile_3](/uploads/c238c03a2a9a0c54e559a994b4448f87/patch-Makefile_3)
https://git.frama-c.com/pub/frama-c/-/issues/260
Frama-C incompatible with Coq 8.8.0
2021-02-22T12:57:44Z
mantis-gitlab-migration
Frama-C incompatible with Coq 8.8.0
ID0002377:
**This issue was created automatically from Mantis Issue 2377. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002377:
**This issue was created automatically from Mantis Issue 2377. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002377 | Frama-C | Opam | public | 2018-05-30 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ramsdell | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i686 | **OS** | Fedora | **OS Version** | 28 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Installation with opam worked well except that it deleted my modern version of Coq!
### Steps To Reproduce :
Install Coq and then install frama-c
https://git.frama-c.com/pub/frama-c/-/issues/263
frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined size...
2021-04-20T17:20:20Z
mantis-gitlab-migration
frama-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/257
Issues while installation of Frama-C using OPAM
2021-02-22T12:57:40Z
mantis-gitlab-migration
Issues while installation of Frama-C using OPAM
ID0002375:
**This issue was created automatically from Mantis Issue 2375. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002375:
**This issue was created automatically from Mantis Issue 2375. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002375 | Frama-C | Opam | public | 2018-05-23 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | NewUser | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Mac OS | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
I am having trouble while installation of frame-C on MacOS. I am trying to install it via OPAM.
I have installed all the dependencies also e.g
(brew install gmp gtk+ gtksourceview libgnomecanvas) but still it is not working.
please see the attached file for detailed error message
## Attachments
- [Terminal_Saved_Output](/uploads/7082f81c36f02c3d9c9831398809ace4/Terminal_Saved_Output)
- [framaC_Output](/uploads/a5124f3a2af8c58f9b21d67edb0a40be/framaC_Output)
- [Frama-CUpgrade](/uploads/2f7687f8cab2e31c03be170677f4b396/Frama-CUpgrade)