frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:24Z
https://git.frama-c.com/pub/frama-c/-/issues/2423
local array decl with non-constant size causes Why error
2021-04-15T09:17:24Z
Jochen Burghardt
local array decl with non-constant size causes Why error
ID0000416:
**This issue was created automatically from Mantis Issue 416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000416:
**This issue was created automatically from Mantis Issue 416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000416 | Frama-C | Plug-in > jessie | public | 2010-02-22 | 2010-02-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
After declaring in a procedure a local array of a size depending on some parameter, when I assert the range-validity, I get (a Kernel warning "No code for function __builtin_alloca" and) a Why error message "Unbound variable bitvector_alloc_table". This doesnt happen for a constant size (see attached file).
## Attachments
- [localFlexArray01.c](/uploads/a05a9a037a93d34b2c583224ef734c52/localFlexArray01.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2422
Uncaught exception: Failure("Unexpected internal region in logic")
2021-04-15T09:17:23Z
Jochen Burghardt
Uncaught exception: Failure("Unexpected internal region in logic")
ID0000424:
**This issue was created automatically from Mantis Issue 424. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000424:
**This issue was created automatically from Mantis Issue 424. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000424 | Frama-C | Plug-in > jessie | public | 2010-03-08 | 2010-03-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie exits with the message <<Uncaught exception: Failure("Unexpected internal region in logic")>> when trying to translate the attached program.
"Uncaught" and "Unexpected" sounds like a bug.
I couldn't find a work-around for it yet.
## Attachments
- [alloc.c](/uploads/7acbbc632e99d6dcc373acc66a071dfe/alloc.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2421
different translation of casted constants in program-code and in assertion
2021-04-15T09:17:22Z
Jochen Burghardt
different translation of casted constants in program-code and in assertion
ID0000433:
**This issue was created automatically from Mantis Issue 433. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000433:
**This issue was created automatically from Mantis Issue 433. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000433 | Frama-C | Plug-in > jessie | public | 2010-03-22 | 2010-03-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file, "my_const" is translated to "1024" in line 8 (C-code),
but to "integer_of_int32(int32_of_integer(1024))" in line 9 (Acsl-code).
As a consequence, Simplify is unable to prove the trivial-looking assertion in line 9 (it seems to lack a rule like
"integer_of_int32(int32_of_integer(x)) <== -maxInt <= x <= +maxInt").
When I remove the cast in line 4, jessie outputs no proof obligation at all, which is (consistent with) what I expected.
## Attachments
- [ftest.c](/uploads/39e21d3026f822775c835db0ba674a74/ftest.c)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/2420
jessie err msg "Uncaught exception" refers to deleted intermediate file "jc/j...
2021-04-15T09:17:22Z
Jochen Burghardt
jessie err msg "Uncaught exception" refers to deleted intermediate file "jc/jc_typing.ml"
ID0000432:
**This issue was created automatically from Mantis Issue 432. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000432:
**This issue was created automatically from Mantis Issue 432. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000432 | Frama-C | Plug-in > jessie | public | 2010-03-22 | 2010-03-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When calling the unix command
<<frama-c -jessie -jessie-no-regions -jessie-why-opt="-exp goal" -jessie-atp simplify ftest.c>>,
I get an error message
<<File "jc/jc_typing.ml", line 2772, characters 25-25:
Uncaught exception: File "jc/jc_typing.ml", line 2772, characters 25-31: Assertion failed
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -why-opt "-exp goal" -locs ftest.cloc ftest.jc>>.
However, the file "jc/jc_typing.ml" does no longer exist when I try to inspect it to find the reason of the error. I guess, it is an intermediate file that has been deleted before I get the shell-prompt.
## Attachments
- [ftest.c](/uploads/b6db060630ddcce4dacf3426c0d5cabf/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/2419
-2147483647<=0 unprovable by Simplify, except in switch
2021-04-15T09:17:24Z
Jochen Burghardt
-2147483647<=0 unprovable by Simplify, except in switch
ID0000415:
**This issue was created automatically from Mantis Issue 415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000415:
**This issue was created automatically from Mantis Issue 415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000415 | Frama-C | Plug-in > jessie | public | 2010-02-22 | 2010-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Simplify can prove neither -2147483648<=0 nor -2147483647<=0, see ftest8() and ftest7() in the attached file. However, it proves -2147483646<=0, see ftest6().
I suggest a jessie cmd-line option to generate -2147483646 rather than -2147483648 as MinInt, in order to circumvent this bug of Simplify, which causes many unprovable no-underflow-obligations in my programs.
Moreover, as a case of a switch, Simplify behaves different on -2147483647<=0: it can prove it there, see case 7 in ftest(). Probably, this is again a problem of Simplify. To ensure this, you could check that the proof obligations you generate are correct.
## Attachments
- [minInt01.c](/uploads/edf84b4457f0e4a42ec5f6bf1a2629ef/minInt01.c)
https://git.frama-c.com/pub/frama-c/-/issues/2407
After ./confugure with --disable-all-staff options and make static, frama-c-M...
2021-02-22T14:04:45Z
Nikolai Kosmatov
After ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashes
ID0000309:
**This issue was created automatically from Mantis Issue 309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000309:
**This issue was created automatically from Mantis Issue 309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000309 | Frama-C | Kernel > ACSL implementation | public | 2009-10-30 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Nikolai_Kosmatov | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
After configuring frama-c with the following options
-----------------------
./configure --disable-constant_propagation --disable-from --disable-gui --disable-impact --disable-inout --disable-ltl_to_acsl --disable-metrics --disable-miel --disable-occurrence --disable-pdg --disable-postdominators --disable-scope --disable-security --disable-semantic_callgraph --disable-slicing --disable-sparecode --disable-syntactic_callgraph --disable-users --disable-value --disable-wp
-----------------------
make
sudo make install
and make static for Myplugin, frama-c-Myplugin.byte crashes with the following output :
------------------------
[kernel] warning: cannot load plug-in Ltl_to_acsl
(incompatible with Beryllium-20090902+dev)
[Myplugin] started...
[kernel] preprocessing with "gcc -w -E -dD -include "/lib/lancPthc.h" merge.c"
[kernel] Unexpected error (Type.StringTbl.Unbound_value("Dynamic.Bool.get \"-warn-unspecified-order\"")).
Please report as 'crash' at http://bts.frama-c.com
------------------------
https://git.frama-c.com/pub/frama-c/-/issues/2406
switch and case expressions must be integer
2021-02-22T14:04:45Z
Virgile Prevosto
switch and case expressions must be integer
ID0000311:
**This issue was created automatically from Mantis Issue 311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000311:
**This issue was created automatically from Mantis Issue 311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000311 | Frama-C | Kernel | public | 2009-11-02 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
following code is happily parsed by frama-c (who at least casts the "a" in the switch to int). It should fails with a type error
- on the switch
- on the case (parameter must be an integer constant according to norm)
float v;
static void fun(void)
{
switch ("a")
{
case "a":
if (v > fabs(1))
{
}
break;
}
}
https://git.frama-c.com/pub/frama-c/-/issues/2402
order of 'decreases' and 'behavior' clauses
2021-02-22T14:04:44Z
Claude Marché
order of 'decreases' and 'behavior' clauses
ID0000327:
**This issue was created automatically from Mantis Issue 327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000327:
**This issue was created automatically from Mantis Issue 327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000327 | Frama-C | Kernel > ACSL implementation | public | 2009-11-10 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cmarche | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
The ACSL grammar specifies that function contracts have the form
function-contract ::= simple-behavior named-behavior* decreases-clause?
however, Frama-C accepts the following without giving any errors nor warnings, and silently ignores the behaviors.
I think that the camlyacc parser should look for the "EOF" terminator of specs to prevent from silently ignore erroneous garbage.
By the way, I think that decreases clauses should be accepted also between requires and behaviors. The reason is that 'decreases t' refer to the value of t in the pre-state, and it seems more natural to me to put clauses realted to the pre-state before those related to the post-state.
/*@ decreases 101-n ;
@ behavior less_than_101:
@ assumes n <= 100;
@ ensures \result == 91;
@ behavior greater_than_100:
@ assumes n >= 101;
@ ensures \result == n - 10;
@*/
int f91(int n) {
if (n <= 100) {
return f91(f91(n + 11));
}
else
return n - 10;
}
### Additional Information :
Pour preciser ma pensee concernant ocamlyacc et logic_parser.mly: l'entree "annot" a la forme
annot: annotation EOF
et je pense que les autres entrees de la grammaire, lexpr et spec, devraient subir le meme traitement.
https://git.frama-c.com/pub/frama-c/-/issues/2400
goto generated by Frama-C and not supported by Jessie
2021-02-22T13:58:15Z
Dillon Pariente
goto generated by Frama-C and not supported by Jessie
ID0000332:
**This issue was created automatically from Mantis Issue 332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000332:
**This issue was created automatically from Mantis Issue 332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000332 | Frama-C | Kernel | public | 2009-11-17 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
When slicing (or simply analyzing) a function like the following one:
void f(int*p,int e,int t,int f,int r)
{
*p = ( (e || (t && f)) && (t || f) );
}
Frama-C translates it into:
/* Generated by Frama-C */
void f(int *p , int e , int t , int f_0 , int r )
{
int tmp ;
if (e) { goto _LOR; }
else {
if (t) {
if (f_0) {
_LOR: /* internal */ ;
if (t) { tmp = 1; }
else { if (f_0) { tmp = 1; } else { tmp = 0; } }
}
else { tmp = 0; }
}
else { tmp = 0; }
}
*p = tmp;
return;
}
with a goto to a inner block.
But Jessie doesn't support this feature:
File "slicef.jc", line 42, characters 7-16: unsupported goto (backward
or to some inner block)
Category of this report is "kernel" as it is let up to Frama-C team to choose between an evolution of Jessie (in order to take this feature into account)
or a change in the way the Kernel (CIL) transforms boolean equations.
https://git.frama-c.com/pub/frama-c/-/issues/2398
redeclaration as different kind of symbol
2021-02-22T13:58:12Z
Claude Marché
redeclaration as different kind of symbol
ID0000358:
**This issue was created automatically from Mantis Issue 358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000358:
**This issue was created automatically from Mantis Issue 358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000358 | Frama-C | Kernel > ACSL implementation | public | 2009-12-08 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cmarche | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
In C, the code
typedef int t;
t t();
fails with error: ‘t’ redeclared as different kind of symbol
The logic parser should produce a similar error as in
/*@ axiomatic A {
logic type t;
logic t t(integer n);
} */
which do not produce any error, but if you do later
//* lemma \forall integer n; t(n) == t(n);
you get user error: syntax error while parsing annotation
which is very difficult to understand !
https://git.frama-c.com/pub/frama-c/-/issues/2397
complete/disjoint behaviors shouldn't accept undefined behaviors
2021-04-15T09:17:28Z
mantis-gitlab-migration
complete/disjoint behaviors shouldn't accept undefined behaviors
ID0000364:
**This issue was created automatically from Mantis Issue 364. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000364:
**This issue was created automatically from Mantis Issue 364. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000364 | Frama-C | Plug-in > jessie | public | 2009-12-24 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yegor | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Processing of following program by Jessie should not succeed. An error should be reported instead.
/*@
behavior foo:
behavior bar:
complete behaviors foo, bar, foobar;
disjoint behaviors foo, bar, foobar;
*/
void f() {
}
https://git.frama-c.com/pub/frama-c/-/issues/2396
Wrong postconditions are "valid according to value analysis"
2021-02-22T13:58:10Z
Guillaume Melquiond
Wrong postconditions are "valid according to value analysis"
ID0000372:
**This issue was created automatically from Mantis Issue 372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000372:
**This issue was created automatically from Mantis Issue 372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000372 | Frama-C | Plug-in > Eva | public | 2010-01-13 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
/*@ ensures \result == 1; */
int main() {
return 0;
}
When clicking on the "ensures" clause, Frama-C GUI (r7298) reports:
This is an ensures clause.
Status: Valid according to value analysis
https://git.frama-c.com/pub/frama-c/-/issues/2395
unsigned long long constant becomes signed
2021-04-15T09:17:27Z
mantis-gitlab-migration
unsigned long long constant becomes signed
ID0000376:
**This issue was created automatically from Mantis Issue 376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000376:
**This issue was created automatically from Mantis Issue 376. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000376 | Frama-C | Plug-in > jessie | public | 2010-01-19 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Mikhail Pritula | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
I have newest why and jessie and simple sample .c file:
/*@ ensures \result == 1;
@ */
int always_one(unsigned long long a) {
if (a <= 0xFFFFFFFFFFFFFFFFull)
return 1;
return 0;
}
I run following command line:
$ frama-c -jessie -jessie-atp simplify ull_constant.c
which produces incorrect lemmas because this big constant becomes -1
https://git.frama-c.com/pub/frama-c/-/issues/2394
Should not call install-kernel-opt on bytecode architectures
2021-02-22T13:58:07Z
mantis-gitlab-migration
Should not call install-kernel-opt on bytecode architectures
ID0000382:
**This issue was created automatically from Mantis Issue 382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000382:
**This issue was created automatically from Mantis Issue 382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000382 | Frama-C | Kernel > Makefile | public | 2010-01-22 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
The “install” target calls unconditionally “install-kernel-opt” which fails on bytecode-only architectures.
Please find attached a patch to fix this little issue.
Regards,
## Attachments
- [0003-Do-not-install-native-Kernel-modules-on-bytecode-arc.patch](/uploads/52da9ae0daa63b793785cc38cc5ddca7/0003-Do-not-install-native-Kernel-modules-on-bytecode-arc.patch)
https://git.frama-c.com/pub/frama-c/-/issues/2392
File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed
2021-02-22T13:58:05Z
mantis-gitlab-migration
File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed
ID0000385:
**This issue was created automatically from Mantis Issue 385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000385:
**This issue was created automatically from Mantis Issue 385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000385 | Frama-C | Kernel | public | 2010-02-01 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | tari3x | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
The attached file crashes Frama-C with the above error. Steps to reproduce:
- load the file in frama-c-gui
- tick Imact->Slicing after impact
- click somewhere on an equality sign in the code
- click "Set Selected"
## Attachments
- [client.i](/uploads/0a9c28d714a2f10e0ca19bc55a5a7322/client.i)
https://git.frama-c.com/pub/frama-c/-/issues/2391
Failure("Function 'From.find_deps_no_transitivity' not registered yet")
2021-02-22T13:58:03Z
mantis-gitlab-migration
Failure("Function 'From.find_deps_no_transitivity' not registered yet")
ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000392 | Frama-C | Plug-in > Eva | public | 2010-02-03 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | djs52 | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Attempting value analysis on a large code base, using -mem-exec to exclude some difficult functions. Running frama-c -val -mem-exec ... seems to complete without error; frama-c-gui with the same options fails with
Unexpected error (Failure("Function 'From.find_deps_no_transitivity' not registered yet"))
https://git.frama-c.com/pub/frama-c/-/issues/2390
assigns clauses are missing from the sliced program
2021-02-22T13:58:02Z
Pascal Cuoq
assigns clauses are missing from the sliced program
ID0000393:
**This issue was created automatically from Mantis Issue 393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000393:
**This issue was created automatically from Mantis Issue 393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000393 | Frama-C | Plug-in > slicing | public | 2010-02-04 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
When the original program contains assigns clauses for functions with code,
the assigns are always omitted from the generated sliced program.
On the other hand pre- and post-conditions seem to be properly included.
In the attached example, the command produces a sliced program that contains:
/*@ requires \valid(p);
behavior default:
ensures (p->a > p->b);
*/
void g_slice_1(las *p )
{
...
The expected behavior is for g_slice_1 to contain in its contract the clause:
assigns p->a;
in addition to the requires and ensures.
### Additional Information :
frama-c -slicing-level 3 -slicing-keep-annotations -slice-assert main -slice-print -ocode slice.foo.c -main main -lib-entry -no-unicode -context-valid-pointers foo.c
# pragma JessieIntegerModel(exact)
typedef struct las { int a; int b; } las;
/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void f(las * p){ p->a = p->b + 1;}
/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void g(las * p) { f(p); }
/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void main(las * p) { g(p);
//@ assert p->a>p->b;
}
https://git.frama-c.com/pub/frama-c/-/issues/2387
imprecision in widening/narrowing for char and short index
2021-02-22T14:04:43Z
Stephane Duprat
imprecision in widening/narrowing for char and short index
ID0000414:
**This issue was created automatically from Mantis Issue 414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000414:
**This issue was created automatically from Mantis Issue 414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000414 | Frama-C | Plug-in > Eva | public | 2010-02-19 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello Stéphane,
> Depending the type of i, the range is not the same.
> The range of i in the loop is [0..10] (for int) or [0..15] for char or
> short.
_____
void main(void)
{
char i=0;
int j=0;
while (i<10) i++;
while (j<10) j++;
}
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
i IN {10; 11; 12; 13; 14; 15; }
j IN {10; }
_____
It's interesting that you noticed this behavior,
because I fixed a comparable problem on short
notice this summer for an intern who had to demo
his plug-in the following week.
Note that the AST for the two loops is different:
i = (char)0;
j = 0;
while ((int )i < 10) {i = (char )((int )i + 1);}
while (j < 10) {j ++;}
CIL transforms the code thus because the C standard
specifies that operators such as ++ do not operate on
types smaller than int, and that values of these types
are implicitly promoted to int in these conditions.
Meanwhile, in the absence of any loop-related
option, the value analysis tries to keep computations
short at the price of precision by using a technique
called "widening". In order to limit the loss of precision,
however, various heuristics are used, including a
syntactic one for the j loop that recognizes that
j IN [0..10] is a good candidate for the loop invariant.
This heuristic does not currently recognize the condition
((int )i < 10) as one where it would be valuable to try
the same kind of invariant.
I have filed this issue as "feature wish" in the Bug Tracking
System, so that it is not forgotten.
http://bts.frama-c.com/view.php?id=325
Pascal
https://git.frama-c.com/pub/frama-c/-/issues/2386
Dgraph.DGraphModel.read_dot
2021-02-22T13:57:57Z
Sylvie Boldo
Dgraph.DGraphModel.read_dot
ID0000431:
**This issue was created automatically from Mantis Issue 431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000431:
**This issue was created automatically from Mantis Issue 431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000431 | Frama-C | Kernel | public | 2010-03-19 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello,
I try to compile the latest svn version (8087) but I can't. I have the following message:
File "src/gui/property_navigator.ml", line 50, characters 18-45:
Error: Unbound value Dgraph.DGraphModel.read_dot
make: *** [src/gui/property_navigator.cmo] Error 2
What my .configure gives is as attached file.
Probably a Makefile problem...
Regards,
Sylvie Boldo
## Attachments
- [toto](/uploads/41db4ba05d9983a1154e110b0d9b1be7/toto)
https://git.frama-c.com/pub/frama-c/-/issues/2384
int32 and real can't be unified
2021-04-15T09:17:26Z
Sylvie Boldo
int32 and real can't be unified
ID0000386:
**This issue was created automatically from Mantis Issue 386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000386:
**This issue was created automatically from Mantis Issue 386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000386 | Frama-C | Plug-in > jessie | public | 2010-02-01 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello,
With the svn version of frama-c and jessie, I have the following problem: an integer cannot be promoted to real inside a function call.
The function \pow takes 2 real numbers. If I give it an int32. Jessie fails to type it.
### Additional Information :
# pragma JessieFloatModel(strict)
double malcolm1() {
double A;
A=2.0;
/*@ assert A==2.; */
/*@ ghost int i = 1; */
/*@ loop invariant A== \pow(2.,i) &&
@ 1 <= i <= 53;
@ loop variant (53-i); */
while (A != (A+1)) {
A*=2.0;
/*@ ghost i++; */
}
/*@ assert A== 0x1.p53; */
}