frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:13:04Zhttps://git.frama-c.com/pub/frama-c/-/issues/838ACSL parsing of greater-than relation with references2021-02-22T13:13:04ZVirgile PrevostoACSL parsing of greater-than relation with referencesID0001921:
**This issue was created automatically from Mantis Issue 1921. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001921:
**This issue was created automatically from Mantis Issue 1921. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001921 | Frama-Clang | Plug-in > clang | public | 2014-09-12 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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** | - |
### Description :
On the following code:
/*@
ensures \result >= x;
*/
int f(int& x) { return ++x; }
/*@
ensures \result == x;
*/
int g(int& x) { return x; }
/*@
ensures \result >= x;
*/
int h(int x) { return x; }
contracts for g and h are correctly parsed, while contract of f produces the following error messages:
tests/specs/ref_spec.cpp:2:23: comparison of incompatible array types
tests/specs/ref_spec.cpp:2:23: expecting a term or predicate
tests/specs/ref_spec.cpp:2:23: the term is not a predicatehttps://git.frama-c.com/pub/frama-c/-/issues/1310ACSL pretty-printer2023-11-21T14:40:58Zmantis-gitlab-migrationACSL pretty-printerID0000859:
**This issue was created automatically from Mantis Issue 859. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000859:
**This issue was created automatically from Mantis Issue 859. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000859 | Frama-C | Kernel > ACSL implementation | public | 2011-06-09 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ckunz | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Inductive predicates are not printed correctly:
predicates of the form:
inductive .... ( ... ) {
case ...;
case ...;
}
are printed as:
predicate .... ( ... ) {
case ...;
case ...;
}
### Additional Information :
A quick fix consists of modifying cil/src/cil.ml as follows:
*** 5676,5682 ****
fprintf fmt "@[<hov 2>logic %a"
(self#pLogic_type None) rt
| None ->
! fprintf fmt "@[<hov 2>predicate"
end;
fprintf fmt " %a%a%a%a"
self#pLogic_var li.l_var_info
--- 5676,5688 ----
fprintf fmt "@[<hov 2>logic %a"
(self#pLogic_type None) rt
| None ->
! begin
! match li.l_body with
! | LBinductive _ ->
! fprintf fmt "@[<hov 2>inductive"
! | _ ->
! fprintf fmt "@[<hov 2>predicate"
! end
end;
fprintf fmt " %a%a%a%a"
self#pLogic_var li.l_var_infohttps://git.frama-c.com/pub/frama-c/-/issues/2654ACSL v18 release is not present in the ACSL github releases page2023-03-31T16:10:59ZDavid CokACSL v18 release is not present in the ACSL github releases pageThe frama-c download page for ACSL: https://frama-c.com/html/acsl.html
lists a V.18, but this version is not present on the ACSL github site: https://github.com/acsl-language/acsl/releases
where v17 is marked as "latest"
I do see that v...The frama-c download page for ACSL: https://frama-c.com/html/acsl.html
lists a V.18, but this version is not present on the ACSL github site: https://github.com/acsl-language/acsl/releases
where v17 is marked as "latest"
I do see that version.tex says v18 - so perhaps no one pushed the button to publish a build of v18.https://git.frama-c.com/pub/frama-c/-/issues/1742actions done with make install -n (svn 10897)2021-02-22T13:39:54ZStephane Dupratactions done with make install -n (svn 10897)ID0000637:
**This issue was created automatically from Mantis Issue 637. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000637:
**This issue was created automatically from Mantis Issue 637. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000637 | Frama-C | Kernel > Makefile | public | 2010-12-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | signoles | **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 Carbon-20110201 |
### Description :
Soit un rep d'installation que j'utilise dans la ligne configure et qui est vide au départ :
./configure -prefix <rep-install>
dans l'arborescence frama-c, après avoir fait le make, je fais un "make install -n" et je m'attend à voir la liste des commandes de recopie dans le rep <rep-install> sans que les commandes soient effectuées (option -n).
Enfin, je constate qu'une certaine partie des commandes ont été réalisées avec pour preuve la création du répertoire lib/frama-c dans <rep-install>.
Stéphane
Le 13/12/2010 10:06, BAUDIN Patrick a écrit :
> Bonjour Stéphane,
> Peut-tu être un peu plus explicite sur l'emplacement de ce répertoire lib
> et sur son contenu (avant et après la commande) ?
> Cdlt,
> Patrick
>> Bonjour,
>> J'ai fait un "make install -n" qui a pris un peu de temps.
>> Après vérification, le répertoire lib a été créé dans le répertoire cible,
>> Cdlt,
>> Stéphanehttps://git.frama-c.com/pub/frama-c/-/issues/2351Addition that may overflow passes verification2021-04-15T09:17:15Zmantis-gitlab-migrationAddition that may overflow passes verificationID0000539:
**This issue was created automatically from Mantis Issue 539. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000539:
**This issue was created automatically from Mantis Issue 539. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000539 | Frama-C | Plug-in > jessie | public | 2010-07-09 | 2010-09-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This line passes in the binary search example:
mid = (low + high) / 2;
## Attachments
- [binary-search.c](/uploads/f10a66f299a024f0a9651a3d77f4d794/binary-search.c)https://git.frama-c.com/pub/frama-c/-/issues/424Add remark about additional axioms for read clauses2022-09-08T08:56:38ZJens GerlachAdd remark about additional axioms for read clausesID0001698:
**This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001698:
**This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001698 | Frama-C | Documentation > ACSL | public | 2014-03-14 | 2016-06-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
As long as WP does not generate foot prints for reads clauses of axiomatic declarations (see
https://bts.frama-c.com/view.php?id=1693), it might be helpful for users to understand, that it is their responsibility to formulate additional axioms/lemmas to express the foot print.
This could be added to Section 2.6.10 of
"ACSL Version 1.8 Implementation in Neon-20140301".https://git.frama-c.com/pub/frama-c/-/issues/1948addr_eq versus = and <> in generated axioms access_update, access_update_neq2021-02-22T13:47:03ZJochen Burghardtaddr_eq versus = and <> in generated axioms access_update, access_update_neqID0001117:
**This issue was created automatically from Mantis Issue 1117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001117:
**This issue was created automatically from Mantis Issue 1117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001117 | Frama-C | Plug-in > wp | public | 2012-03-12 | 2012-11-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pherrmann | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
I ran "frama-c -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -wp-proof alt-ergo -no-unicode -wp-warnings -wp-out ./out ftest.c" on the attached program and inspected the generated file "out/store_ftest_post_1_po_ergo.why".
In the proof obligation for c-source line 14, the update operator a[i<-v] is used with e.g. addr_shift(s_0,0) substituted for i. In the axioms access_update and access_update_neq, arguments at position i are compared by built-in equality (and disequality <>).
However, terms starting with "addr_shift" are usually compared by "addr_eq", e.g. in the translation of lemma l.
I suggest to check whether the mentioned axioms should be weakened to:
axiom access_update : (forall a:'a1 farray.(forall i:int.(forall j:int.(forall v:'a1.(addr_eq(i,j) -> a[i<-v][j]=v)))))
axiom access_update_neq : (forall a:'a1 farray.(forall i:int.(forall j:int.(forall v:'a1.((not addr_eq(i,j)) -> (a[i<-v][j]=a[j]))))))
If not, I suggest to check whether addr_eq is in fact the same as =, and to drop the former for sake of simplicity.
## Attachments
- [ftest.c](/uploads/cd05b6376c9c0e2eb054fdb51936c97c/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/805advanced adress arithmetic causes loss of source location2021-02-22T13:12:24ZJochen Burghardtadvanced adress arithmetic causes loss of source locationID0001802:
**This issue was created automatically from Mantis Issue 1802. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001802:
**This issue was created automatically from Mantis Issue 1802. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001802 | Frama-Clang | Plug-in > from | public | 2014-06-06 | 2015-02-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
output of "frama-c -deps from.c -slevel 10":
...
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main:
publc2 FROM publc1
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
However, if "publc1" is located e.g. at address 0x30000, then "p" would point to 0x30004, that is, (possibly) to "secret1", which wasn't mentioned as source location by FromAnalysis.
## Attachments
- [from19.cpp](/uploads/bdfbcb6fc20f5ccd3b855d20daa083f8/from19.cpp)https://git.frama-c.com/pub/frama-c/-/issues/2407After ./confugure with --disable-all-staff options and make static, frama-c-M...2021-02-22T14:04:45ZNikolai KosmatovAfter ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashesID0000309:
**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/1622After ./confugure with --disable-all-staff options, make holds2021-02-22T13:36:13ZNikolai KosmatovAfter ./confugure with --disable-all-staff options, make holdsID0000305:
**This issue was created automatically from Mantis Issue 305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000305:
**This issue was created automatically from Mantis Issue 305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000305 | Frama-C | Kernel > configure | public | 2009-10-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Nikolai_Kosmatov | **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 :
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
-----------------------
and trying make or make clean, got the following output :
nk@mypc:~/frama-c$ make
Generating src/lib/dynlink_common_interface.ml
Generating src/kernel/config.ml
Generating ptests/ptests_config.ml
Generating share/Makefile.kernel
Generating .depend
hanging with no visible action on .depend for hours.https://git.frama-c.com/pub/frama-c/-/issues/1334Aggregate logic types containing only C types2024-03-16T08:11:35Zmantis-gitlab-migrationAggregate logic types containing only C typesID0000835:
**This issue was created automatically from Mantis Issue 835. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000835:
**This issue was created automatically from Mantis Issue 835. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000835 | Frama-C | Kernel > ACSL implementation | public | 2011-05-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | proux | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
According to section 2.2.7 of current ACSL implementation
documentation
http://frama-c.com/download/acsl-implementation-Carbon-20110201.pdf
it would be possible to use for example arrays of integers:
"Aggregate types can be declared in logic, and their contents may be any logic types themselves."
but when trying so, we got an error "not a C type".
Looking at type logic_type in cil/src/cil_types.mli
I understand that actually implementing what the documentation
says may require a non negligible amount of work
and I don't expect it anytime soon.
But putting a "not yet implemented" warning or something like that
in the implementation documentation would be nice.https://git.frama-c.com/pub/frama-c/-/issues/2196alias between int* and uint* handled incorrectly2021-04-15T09:17:06ZJochen Burghardtalias between int* and uint* handled incorrectlyID0000829:
**This issue was created automatically from Mantis Issue 829. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000829:
**This issue was created automatically from Mantis Issue 829. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000829 | Frama-C | Plug-in > jessie | public | 2011-05-18 | 2011-05-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The manual "jessie-tutorial-Carbon-beta.pdf" allows casts between pointer types (p.22). However, in the attached program, the property "*x == \old(*x)" of the function ftest() can be verified under SeparationPolicy(none), although ftest() modifies *x via its (possible) alias *y. A reason for this behavior is that x and y point to different types, viz. int and uint (if y is made an int, too, the bug vanishes).
As a consequence, "p == \old(p)" can be proven for main(), although running the program reveals that p changes from 0 to 123. A side remark: type incompatibility uint* vs. int* seems to be unchecked in the initialization in line 14; no cast was needed there.
## Attachments
- [ftest.c](/uploads/2fd0ddaf71c2c701d8720d61b435b17e/ftest.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2692[alias] expose more functions2024-03-14T10:51:28ZJan Rochel[alias] expose more functionsCopied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to ...Copied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to iterate over all equivalence classes, and I think only raw access to the graph allows this).
More precisely:
* `get_lval` / `find_aliases` now only returns variable aliases; there is `reconstruct_lvals` internally to compute all the aliases but it is not exposed (it is used by find_all_aliases, but that also brings aliases from other equivalence classes);
* edge labels are not exposed, so it is not possible to distinguish between pointer and field edges from outside the plugin, making raw access to the graph impossible to do correctly
Would it be possible to expose `EdgeLabel `and (an equivalent of) `reconstruct_lvals` from the plugin's API?Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2677Alias plugin does not propagate inside records and arrays2024-03-09T12:39:09ZBasile ClémentAlias plugin does not propagate inside records and arraysThe Alias plug-in does not seem to know that if `p` points to `x`, then `x.ptr` and `p->ptr` are the same. This is also the case for pointers to arrays of pointers (with `*(*)[]` types).
The attached files should reproduce the issue; wh...The Alias plug-in does not seem to know that if `p` points to `x`, then `x.ptr` and `p->ptr` are the same. This is also the case for pointers to arrays of pointers (with `*(*)[]` types).
The attached files should reproduce the issue; when running them through `frama-c -alias` I get
```
[alias] May-aliases at the end of function main:
{ a; t.field } { z; q } { z->field; b } { q->field; n }
```
which places the pointers `a`, `b` and `n` in different classes even though we can check by running the program that `a == b` and `a == n` hold at the end of the `main` function.
Note that in the plug-in's README, "pointer arithmetic, and array and structure accesses" is listed under "imprecisely-supported constructs", so this may be expected — however it would be surprising to me that "imprecisely-supported" means "unsound".
[records.c](/uploads/8864c33684705ab86d725ccbe5ba3e38/records.c)
[arrays.c](/uploads/11360a2237d2be19e3359dcfabe7157d/arrays.c)Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2666Alias plugin's `Abstract_state` API requires using private `Alias__Abstract_s...2023-11-06T08:47:52ZBasile ClémentAlias plugin's `Abstract_state` API requires using private `Alias__Abstract_state` moduleThe Alias plugin exposes [the `Abstract_state` module](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/abstract_state.mli) through [`API.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.ml...The Alias plugin exposes [the `Abstract_state` module](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/abstract_state.mli) through [`API.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.mli).
However, OCaml doesn't know that the modules `G` and `LSet` used in the `Abstract_state` module are the same as those exposed in the `API` module, even though [they are](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.ml#L26-28), because the `.mli` do not expose this information. To use `API.Abstract_state` in a meaningful way, the `G` and `LSet` modules must be accessed through the private `Alias__Abstract_state` module generated by `dune`.Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/1914Alignment of global character arrays2021-02-22T13:45:59ZDavid DelmasAlignment of global character arraysID0000873:
**This issue was created automatically from Mantis Issue 873. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000873:
**This issue was created automatically from Mantis Issue 873. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000873 | Frama-C | Plug-in > Eva | public | 2011-06-28 | 2013-02-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
With the attached source file,
$ frama-c tab_char.c -val
produces the (correct) output :
[value] Called Frama_C_show_each_Alignment(
{{ &"WARNING: address possibly non word aligned" ;}},
{{ &t ;}})
However, adding options -machdep ppc_32_diab does not change this output, although character arrays have a default alignment of 4 with the Diab C cross-compiler for PowerPC.
It would be useful to have -machdep ppc_32_diab take this specific feature into account.
## Attachments
- [tab_char.c](/uploads/1b6648205d05612a39c5e0f2dfdcbe24/tab_char.c)https://git.frama-c.com/pub/frama-c/-/issues/1197Allow starting coq from Frama-C GUI also for proven obligations2021-02-22T13:30:12ZJens GerlachAllow starting coq from Frama-C GUI also for proven obligationsID0001623:
**This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001623:
**This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001623 | Frama-C | Plug-in > wp | public | 2014-01-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, OSX | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Currently it is not possible to start the codide from the Frama-C GUI
for a proof obligation that has already been proven by Coq.
However, it would be desirable to do so in order to improve/refactor an already existing proof.https://git.frama-c.com/pub/frama-c/-/issues/2103alteration of user-defined assigns clauses2021-02-22T13:51:03ZDavid Delmasalteration of user-defined assigns clausesID0000468:
**This issue was created automatically from Mantis Issue 468. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000468:
**This issue was created automatically from Mantis Issue 468. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000468 | Frama-C | Kernel | public | 2010-05-03 | 2011-10-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The builtin.* source files distributed together with Frama-C define the below prototypes :
builtin.c :
//@ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
void Frama_C_update_entropy(void);
builtin.h :
/*@ assigns \result \from a, b, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int Frama_C_nondet(int a, int b);
[...]
/*@ assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int Frama_C_interval(int min, int max);
Let us prompt the below commands on the attached assigns.c source file :
SHARE=`frama-c -print-path`
export CPP="gcc -C -E -I$SHARE"
frama-c assigns.c $SHARE/builtin.c -print -ocode print_assigns.c
The generated print_assigns.c source file defines the following behaviors :
/*@ behavior default:
assigns Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
extern void Frama_C_update_entropy(void) ;
/*@ behavior default:
assigns Frama_C_entropy_source;
assigns \result \from a, b, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int Frama_C_nondet(int a , int b )
{ [...] }
/*@ behavior default:
assigns Frama_C_entropy_source;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int Frama_C_interval(int min , int max )
{ [...] }
Theses clauses are correct, but they spoil the precision of the value analysis plug-in on the interpretation of \from clauses. See the "Additional Information" field for a detailed explanation by Pascal Cuoq.
### Additional Information :
Message from Pascal Cuoq :
-----------------------------------
J'ai dû transformer ton fichier ainsi :
int Frama_C_entropy_source ;
/*@ behavior default:
// assigns Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
extern void Frama_C_update_entropy(void) ;
/*@ behavior default:
// assigns Frama_C_entropy_source;
assigns \result \from a, b, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int Frama_C_nondet(int a , int b )
{
int tmp ;
Frama_C_update_entropy();
...
et ce pour chaque ligne d'assigns qui était ainsi redondante.
En effet chaque ligne d'assigns est sensée être vérifiée indépendamment
des autres, donc cela ne change pas le sens d'écrire les choses en
double comme c'était dans le fichier, mais l'analyse de valeurs ne
cherche pas à être trop maline sur les assigns qui ont une intersection
non vide. Quand elle voit
assigns Frama_C_entropy_source ;
elle note que cette variable est calculée à partir de toutes les variables
accessibles, et comme les inputs d'une fonction incluent les inputs
des appelées, c'est toutes les fonctions appelant directement ou
indirectement celles qui sont sur-spécifiées qui semblent lire toute la
mémoire.
Si ces assigns ont été générés par une transformation de Frama-C
à partir d'assigns non redondants, alors ce n'est pas vraiment ta faute
et c'est un bug qu'il convient de rapporter.
## Attachments
- [assigns.c](/uploads/f575bc6962662c98aaca01d9ab3e14f4/assigns.c)https://git.frama-c.com/pub/frama-c/-/issues/112alt-ergo goals generated directly / via why3 differ in provability2021-02-22T12:53:52ZJochen Burghardtalt-ergo goals generated directly / via why3 differ in provabilityID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002353 | Frama-C | Plug-in > wp | public | 2018-02-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
I generated an Alt-Ergo proof obligation for the ensures clause "xxx" (line 1140) of the attached program "search_n_standalone.c" (which was obtained from "search_n" in "Acsl by example" by "gcc -E -C"). When I did this directly (see attached script "fd"), it was proven without problems. However, when I did this via Why3 (see script "fw"), Alt-Ergo responded "Don't know" after 0.1 seconds.
In order to compare both mlw files given to Alt-Ergo, I moved the goal of the via-Why3 file into the direct file; it became provable there. Removing as many axioms and definitions as possible while keeping the (non-)provability, I obtained the files "xxx_direct.mlw" and "xxx_via_why3.mlw". It seems that the former defines and uses "shift_sint32", while the latter does not (it uses "shift" instead). Probably, this is the reason for the different outcomes of Alt-Ergo.
Although the observed issue may not be bug (both mlw files may be semanically equivalent), it might be desirable to unify the proof obligations given to Alt-Ergo on different pathways.
## Attachments
- [search_n_standalone.c](/uploads/79defa5986c7ebb10060cb2d8013dd27/search_n_standalone.c)
- [fd](/uploads/2325b1feb2a0e2c6bc2768f1552ecbf9/fd)
- [fw](/uploads/ade985efb5f8ea0601fa91f90ec1f340/fw)
- [xxx_direct.mlw](/uploads/49efc095c1124c4e87c110c2b7a10bb7/xxx_direct.mlw)
- [xxx_via_why3.mlw](/uploads/28204d54407af26ed64d8841005b5cef/xxx_via_why3.mlw)https://git.frama-c.com/pub/frama-c/-/issues/102alt-ergo support in Frama-C 20 beta2021-04-14T07:30:38ZJens Gerlachalt-ergo support in Frama-C 20 betaID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002484 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a hint to (better) describe the transition from using alt-ergo in Frama-C 19 and 20.
If it is already described, then I apologize.
In Frama-C 19 and before one uses
-wp-prover alt-ergo for the native interface and
-wp-prover why3:alt-ergo for the Why3 interface
In Frama-C 20 the respective options are
-wp-prover native:alt-ergo for the native interface and
-wp-prover alt-ergo
I propose that it is described with other things in a short transition document.Loïc CorrensonLoïc Correnson