frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T12:54:48Z
https://git.frama-c.com/pub/frama-c/-/issues/145
Obfuscator does not obfuscate argument name of function pointers
2021-02-22T12:54:48Z
Virgile Prevosto
Obfuscator does not obfuscate argument name of function pointers
ID0002433:
**This issue was created automatically from Mantis Issue 2433. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002433:
**This issue was created automatically from Mantis Issue 2433. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002433 | Frama-C | Plug-in > obfuscator | public | 2019-03-26 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 19-Potassium | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
Using the code given in attachment, the output of `frama-c -obfuscate obf.c` does leak the name of my_arg, the formal parameter of the function pointer typedef'd as func.
## Attachments
- [obf.c](/uploads/ca38c133057346e3b3415c76f21fd0dd/obf.c)
https://git.frama-c.com/pub/frama-c/-/issues/342
There is a typo in description of plug-in: "objuscator" instead of "obfuscator".
2022-09-08T08:56:38Z
mantis-gitlab-migration
There is a typo in description of plug-in: "objuscator" instead of "obfuscator".
ID0002269:
**This issue was created automatically from Mantis Issue 2269. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002269:
**This issue was created automatically from Mantis Issue 2269. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002269 | Frama-C | Plug-in > obfuscator | public | 2017-01-12 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | none | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
$ frama-c -plugins
...
Obfuscator objuscator for confidential code (-obfuscator-h)
...
And there is the same typo in GUI: "Objuscator for confidential code".
### Steps To Reproduce :
1. In command line enter:
frama-c -plugins
2. In GUI select Analyses -> Obfuscator.
https://git.frama-c.com/pub/frama-c/-/issues/1184
Obfuscator for C Labels
2021-02-22T13:22:32Z
Patrick Baudin
Obfuscator for C Labels
ID0001562:
**This issue was created automatically from Mantis Issue 1562. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001562:
**This issue was created automatically from Mantis Issue 1562. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001562 | Frama-C | Plug-in > obfuscator | public | 2013-11-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
C Label names to to be obfuscated.
### Additional Information :
> frama-c -obfuscate file.c
int main(int f1)
{
int V1;
V1 = 0;
if (f1) goto end;
V1 ++;
end: ;
return V1;
}
https://git.frama-c.com/pub/frama-c/-/issues/1220
Obfuscator for tags names in ACSL terms, properties, behaviors
2023-11-21T14:40:58Z
Patrick Baudin
Obfuscator for tags names in ACSL terms, properties, behaviors
ID0001563:
**This issue was created automatically from Mantis Issue 1563. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001563:
**This issue was created automatically from Mantis Issue 1563. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001563 | Frama-C | Plug-in > obfuscator | public | 2013-11-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Tags names in ACSL terms, properties, behaviors need to be obfucated.
### Additional Information :
> frama-c -obfuscate file.c
/*@ behavior bhv:
exits never: \false;
complete behaviors bhv; */
int main(int f1)
{
int V1;
V1 = 0;
if (f1) goto end;
V1 ++;
/*@ assert property: V1 ? 1; */ ;
end: ;
return V1;
}
https://git.frama-c.com/pub/frama-c/-/issues/1606
obfuscator loses link between logic and C variables
2021-02-22T13:35:47Z
Virgile Prevosto
obfuscator loses link between logic and C variables
ID0000250:
**This issue was created automatically from Mantis Issue 250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000250:
**This issue was created automatically from Mantis Issue 250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000250 | Frama-C | Plug-in > obfuscator | public | 2009-09-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
on the code below,
//@ requires \valid(p);
void f(int * p);
int main(int * p)
{ f(p); }
executing frama-c -obfuscate t.c
returns
/*@ requires \valid(V1);
*/
extern void F1(int *G1 ) ;
int main(int *V3 )
{
int V2 ;
F1(V3);
V2 = 0;
return (V2);
}
i.e. the variable in the requires clause is not bound to the parameter of F1 anymore. It should be requires \valid(G1) instead.