frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-05-16T06:53:50Zhttps://git.frama-c.com/pub/frama-c/-/issues/2646OPAM installation on macOS fails2023-05-16T06:53:50ZvarosiOPAM installation on macOS fails<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
To install correctly using OPAM on macOS Ventura 13.2 on x64 following - https://frama-c.com/html/get-frama-c.html
### Actual behaviour
After running **opam install frama-c**, I got:
```
> <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
> -> removed conf-gtk2.1
> -> installed conf-gtk2.1
> -> retrieved frama-c.21.1 (cached)
> [ERROR] The compilation of frama-c.21.1 failed at "make -j11".
>
> #=== ERROR while compiling frama-c.21.1 =======================================#
> # context 2.1.4 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#0c15cf29
> # path ~/.opam/default/.opam-switch/build/frama-c.21.1
> # command ~/.opam/opam-init/hooks/sandbox.sh build make -j11
> # exit-code 2
> # env-file ~/.opam/log/frama-c-37505-febf41.env
> # output-file ~/.opam/log/frama-c-37505-febf41.out
> ### output ###
> # [...]
> # Ocamlc src/plugins/qed/hcons.cmo
> # Ocamlc src/plugins/qed/listmap.cmo
> # Ocamlc src/plugins/qed/listset.cmo
> # Ocamlc src/plugins/qed/intmap.cmo
> # Ocamlc src/plugins/qed/intset.cmo
> # File "src/plugins/markdown-report/sarif.ml", line 31, characters 17-30:
> # Error: Unbound type constructor Yojson.Safe.t
> # make: *** [src/plugins/markdown-report/sarif.cmo] Error 2
> # make: *** Waiting for unfinished jobs....
> # Ocamlc src/plugins/qed/idxmap.cmo
> # AR src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
> # RANLIB src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: not installed previously
- OS name: macOS
- OS version: Ventura 13.2 on x64Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/53Documentation for Report plug-in is not correct2021-03-29T11:50:09ZvarosiDocumentation for Report plug-in is not correct- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you insta...- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0 (Titanium)
- Plug-in used: Report
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
1. I open the Documentation from Frama-C official page: https://frama-c.com/download/frama-c-user-manual.pdf
2. Paragraph: **10.3.2 Rules**
3. I see a JSON there. This JSON is in curly brackets "{ ... }". And there is a "plugin" property.
4. I run:
`frama-c -report-rules report_rules.json src/main.c -wp -wp-rte -then -report -then -report-classify`
with report_rules.json file:
```
{
"plugin": "wp" ;
["unknown"]: "[a-zA-Z0-9]*_ensures"
}
```
as it is on the documentation.
4. I got:
> [report] report_rules.json:2: User Error: un-recognised token (at ";")
So first I need to change ";" for ",".
5. Then I got:
> [report] report_rules.json:3: User Error: missing name (at "[")
Then I added square brackets "[ {...} ]" gave another error:
> [report] report_rules.json:3: User Error: missing name (at "[")
5. It has problems with "plugin" property also.
6. With lots of experimentation and time lost I got to some version that works:
```
[
{"unknown": "[a-zA-Z0-9]*_ensures"}
]
```
Paragraph 10.3.2 Rules of the documentation is not correct in my point of view. It would be great if there is a tested and working example there. This will save user's time. Currently I still don't know how to structure this JSON so it work with all of its features.
# Expected behaviour
Documentation to meet actual JSON format.