pub issueshttps://git.frama-c.com/groups/pub/-/issues2024-03-16T08:11:35Zhttps://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/1316Results differ between value analysis and GCC on bitfields2024-03-15T09:13:18ZBenjamin MonateResults differ between value analysis and GCC on bitfieldsID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000890 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **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 Nitrogen-20111001 |
### Description :
On the program
==bug.i==============
union U0 {
unsigned short f0 ;
int f1 ;
int f2 : 5 ;
unsigned char const f3 ;
};
unsigned short G0 ;
int G1 ;
int G2;
unsigned char G3 ;
union U0 G={(unsigned short)65532U};
int main() {
G0=G.f0;
G1=G.f1;
G2=G.f2;
G3=G.f3;
printf("%d %d %d %d : %d\n",G0,G1,G2,G3,G2==-4);
return (G2==-4);
}
=========================
frama-c -val bug.i
returns:
===
[value] Values for function main:
G0 ? {65532}
G1[bits 0 to 15] ? {65532}
[bits 16 to 31] ? {0}
G2 ? {28}
G3# ? {65532} misaligned 0%16
__retres ? {0}
===
but gcc bug.i && ./a.out ; echo $?
displays :
===
65532 65532 -4 252 : 1
1
===
They do not agree on the result nor on the value of G2.https://git.frama-c.com/pub/frama-c/-/issues/2639Parse-print-reparse error with ranges2024-03-14T16:37:09ZNikolai KosmatovParse-print-reparse error with ranges## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after pa...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses in ranges).
[f.c](/uploads/dac68b95adf9d3c2c83b7b3ec9ce5898/f.c)
Here is the example
```
// Run frama-c on this file and pretty-print it:
// frama-c f.c -print -no-unicode -ocode f_printed.c
// Run on the resulting pretty-printed file:
// frama-c f_printed.c
typedef unsigned char uchar;
typedef unsigned long ulong;
typedef unsigned char *pchar;
uchar *Ref;
uchar Array[100];
/*@ ghost ulong FCG_Var1[1000]; */
/*@ ensures
sep1:
\let Ref_range = Ref + (0 .. (1 << (size)) - 1);
\let PROP = \forall integer MyNum;
\let myrange = (0 .. (6 - 1));
\let Var2 = &Array[FCG_Var1[MyNum]];
\let CASE_i = 0 <= MyNum < 10;
\let PROP_i =
\separated(Ref_range, Var2 + myrange);
CASE_i ==> PROP_i;
PROP;
*/
static uchar myfun(pchar p_array, short index, uchar size)
{
uchar __retres;
return __retres;
}
```
Here is the error message:
```
[kernel] Parsing f_printed.c (with preprocessing)
[kernel:annot-error] f_printed.c:11: Warning: unexpected token '..'
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "f_printed.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```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/136817514, -unspecified-access and if (*p = (*p < 3)) (csmith)2024-03-12T17:06:13ZPascal Cuoq17514, -unspecified-access and if (*p = (*p < 3)) (csmith)ID0001114:
**This issue was created automatically from Mantis Issue 1114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001114:
**This issue was created automatically from Mantis Issue 1114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001114 | Frama-C | Kernel | public | 2012-03-10 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **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 Oxygen-20120901 |
### Description :
In the program below, line 6 is as innocuous as line 5, but:
$ bin/toplevel.opt -val -unspecified-access t.c
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:6:[kernel] warning: Unspecified sequence with side effect:
/* <- *p p */
tmp = *p < 3;
/* *p <- tmp p */
*p = tmp;
...
t.c:6:[kernel] warning: undefined multiple accesses in expression. assert \separated(p, p);;
int x, *p;
main(){
p = &x;
*p = (*p < 3);
if (*p = (*p < 3))
x = 4;
}https://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/cabrnet/-/issues/33Use Captum for Smoothgrads2024-03-07T10:20:44ZRomain Xu-DarmeUse Captum for SmoothgradsRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/22Add .yml files for StanfordCars2024-03-06T13:35:44ZJules SoriaAdd .yml files for StanfordCarsIn `configs/prototree/` the .yml files are configured for the CUB200 dataset - create two subfolders with configuration files for both CUB200 and StandfordCarsIn `configs/prototree/` the .yml files are configured for the CUB200 dataset - create two subfolders with configuration files for both CUB200 and StandfordCarsJules SoriaJules Soriahttps://git.frama-c.com/pub/frama-c/-/issues/2690[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL2024-03-06T11:53:41Zkwaxer[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enu...### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
```
3. Run WP plugin selecting Isabelle/HOL as a backend: `frama-c -wp -wp-prover=why3:isabelle -wp-interactive=fix -wp-cache=none test.h`
### Expected behaviour
Earlier versions of Frama-C (e.g. 27.1) produce the following output:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 0
Isabelle 2022: 1 (8.1s)
```
with the theory
```isabelle
theory lemma_enumeration_length imports Why3.Why3 begin
why3_open "lemma_enumeration_length.xml"
why3_vc wp_goal
using assms L_enumeration_def
by (induction i) (simp_all add: facts.length_concat length_cons length_nil)
why3_end
end
```
### Actual behaviour
Frama-C 28.0 produces the following:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failure] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Failed: 1
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *28.0 (Nickel)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04.4 LTS*
### Additional information (optional)
`-wp-msg-key why3_api` gives the following error trace:
```
[wp] Failure: [Why3 Error] anomaly: Sys_error(".../.frama-c/wp/interactive/lemma_enumeration_length/.xml: No such file or directory")
Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
Called from Frama_c_kernel__Command.pp_to_file in file "src/libraries/utils/command.ml", line 31, characters 13-35
Called from Wp__ProverWhy3.prepare in file "src/plugins/wp/ProverWhy3.ml", line 1339, characters 6-130
Called from Wp__ProverWhy3.interactive in file "src/plugins/wp/ProverWhy3.ml", line 1352, characters 8-37
Called from Wp__ProverWhy3.build_proof_task in file "src/plugins/wp/ProverWhy3.ml", line 1413, characters 8-59
```
There is an unexpected slash right the before `.xml` file extension.https://git.frama-c.com/pub/frama-c/-/issues/1295r13586 Spurious "assert \separated(...)" (csmith)2024-03-05T16:33:49ZPascal Cuoqr13586 Spurious "assert \separated(...)" (csmith)ID0000832:
**This issue was created automatically from Mantis Issue 832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000832:
**This issue was created automatically from Mantis Issue 832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000832 | Frama-C | Kernel | public | 2011-05-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **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 Nitrogen-20111001 |
### Description :
file t.c:
int a, *G;
int g(int x, int y)
{
return x + y;
}
main(int c, char **v){
G = &a;
*G =
(a < (g((0U ||
(((a ^ a) <= a) < ((*G) || a))), 5)));
return a;
}
$ ~/ppc/bin/toplevel.byte -val -unspecified-access t.c
t.c:13:[kernel] warning: Unspecified sequence with side effect:
/* <- a G *G */
if (*G) { tmp = 1; } else { if (a) { tmp = 1; } else { tmp = 0; } }
/* <- a a a */
/* <- */
tmp_0 = g((((a ^ a) <= a) < tmp) != 0,5);
/* *G <- G a */
*G = a < tmp_0;
...
t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,& a);
t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,G);
...
The program is completely defined, g has no side-effects.https://git.frama-c.com/pub/cabrnet/-/issues/34Catch errors in the main while collecting the apps2024-03-05T08:15:52ZAlban GrastienCatch errors in the main while collecting the appsIf an app is buggy (e.g., its import list is incorrect), it is impossible to call another app. It'd be good to catch this kind of errors and maybe print a warning.If an app is buggy (e.g., its import list is incorrect), it is impossible to call another app. It'd be good to catch this kind of errors and maybe print a warning.Alban GrastienAlban Grastienhttps://git.frama-c.com/pub/cabrnet/-/issues/30Add support for file logging instead of std output2024-03-04T17:09:56ZRomain Xu-DarmeAdd support for file logging instead of std outputRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/32Constants for common filenames2024-03-04T17:09:41ZAlban GrastienConstants for common filenamesTo retrieve the config file of a model in a folder `checkpoint`, we currently use the command
```model_config = os.path.join(checkpoint, "model_config.yml")```
It would be good to have a constant that records what the standard name for...To retrieve the config file of a model in a folder `checkpoint`, we currently use the command
```model_config = os.path.join(checkpoint, "model_config.yml")```
It would be good to have a constant that records what the standard name for this type of file is:
```model_config = os.path.join(checkpoint, CaBRNet.MODEL_CONFIG_FILENAME)```
(or similar). Also applies to `"model_state.pth"`, `"dataset.yml"`, `"training.yml"`, `"visualization.yml"`, and the `"final"` and `"best"` checkpoint folders.Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/frama-c/-/issues/2673[WP] non-matching of strategies with logical operators2024-03-04T10:14:59ZNikolai Kosmatov[WP] non-matching of strategies with logical operators### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,...### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,tip -wp-timeout 1 -wp-prop post`
to apply a strategy with Split does not seem to accept the pattern and to match the precondition with logical operations `&&` and `||`
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
strategy SplitProver:
FastAltErgo,
\tactic("Wp.split"
,\pattern( ((A && B) || (C && D)) )
,\children(EagerAltErgo)
),
EagerAltErgo;
proof SplitProver: post;
```
### Expected behaviour
According to documentation, ACSL logical operations are recognized and after a successful matching, a script is created with two subgoals (to be completed).
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam from GIT pub
- Frama-C version: first version of the strategy mechanism (https://git.frama-c.com/pub/frama-c.git#3396bd), also the recent update on master on pub (by the branch fix/wp/strategies)
- Plug-in used: WP with Why3 1.6.0 and Alt-Ergo 2.4.3
- OS name: Ubuntu
- OS version: 22.04Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/cabrnet/-/issues/31Move visualisation directory to visualization2024-03-04T10:03:27ZRomain Xu-DarmeMove visualisation directory to visualizationhttps://git.frama-c.com/pub/cabrnet/-/issues/28Copy the visualizer config file in the checkpoints so that they are easy to r...2024-03-04T09:05:13ZAlban GrastienCopy the visualizer config file in the checkpoints so that they are easy to retrieve when we restart a trainingRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/19Move download_examples and fetch_legacy_repos elsewhere2024-03-01T11:19:55ZRomain Xu-DarmeMove download_examples and fetch_legacy_repos elsewhereThese scripts should be moved into relevant directories.These scripts should be moved into relevant directories.Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/26Specify config directory as an alternative to individual files2024-02-29T12:02:49ZRomain Xu-DarmeSpecify config directory as an alternative to individual filesIt is sometimes tedious to specify multiple YML files from the same configuration directory. It would be nice to offer an optional `--config-dir` alternative. This would mean that each script expects specific filenames for the different ...It is sometimes tedious to specify multiple YML files from the same configuration directory. It would be nice to offer an optional `--config-dir` alternative. This would mean that each script expects specific filenames for the different files:
+ For `train.py` and `import.py`, we would expect `model.yml`, `dataset.yml`, `training.yml` and `visualization.yml`
+ For `evaluate.py`, we would expect `model.yml`, `model_state.pth` or `legacy_state.pth`, `dataset.yml`
+ For `explain_local.py`, we would expect `model.yml`, `model_state.pth`, `dataset.yml` and `visualization.yml`
+ For `explain_global.py`, we would expect`model.yml` and `model_state.pth`https://git.frama-c.com/pub/cabrnet/-/issues/24Visualization.yml in checkpoint2024-02-29T12:02:38ZAlban GrastienVisualization.yml in checkpointCould we include `visualization.yml` in the checkpoint? Makes the `resume-from` encore plus awesome.Could we include `visualization.yml` in the checkpoint? Makes the `resume-from` encore plus awesome.Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/27Change model.yml to model_arch.yml2024-02-29T12:02:20ZRomain Xu-DarmeChange model.yml to model_arch.ymlIt appears that the name model.yml can be somewhat confusing as it **may** imply that the file contains everything necessary to build and initialize the model, when it actually only the information regarding the model architecture.
To em...It appears that the name model.yml can be somewhat confusing as it **may** imply that the file contains everything necessary to build and initialize the model, when it actually only the information regarding the model architecture.
To emphasize this, we could rename model.yml into model_arch.yml in the documentation and the provided examples.