frama-c merge requestshttps://git.frama-c.com/pub/frama-c/-/merge_requests2022-05-17T08:03:21Zhttps://git.frama-c.com/pub/frama-c/-/merge_requests/6Unmarshal: Hide type-breaking code behind Sys.opaque_identity2022-05-17T08:03:21ZVincent LavironUnmarshal: Hide type-breaking code behind Sys.opaque_identitySee description in #2594.See description in #2594.25 (Manganese)François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/merge_requests/12[gui] Fix menu item labels alignment2024-03-27T06:14:24ZSylvain[gui] Fix menu item labels alignmentHello, thank you for providing Frama-C.
This MR fixes menu items alignments at the top of the GUI for items with a picture. They are currently centered, which gives them a quite uncommon style:
![image](/uploads/5caaddebc07f71599de2dc8...Hello, thank you for providing Frama-C.
This MR fixes menu items alignments at the top of the GUI for items with a picture. They are currently centered, which gives them a quite uncommon style:
![image](/uploads/5caaddebc07f71599de2dc8accf45bb1/image.png)
With my fix, it’s like this:
![image](/uploads/93c5b2cdb002b9d85899001ad23ac489/image.png)
I wasn’t able to remove the margins on the left and on the right though.
The fix is to change `box#add` to `box#pack` when creating the menu items. It is on my fork: https://git.frama-c.com/Frigory33/frama-c
I also removed some unnecessary labeled arguments which didn’t solve the issue.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/merge_requests/11Issue #2687: Fix Makefile escaping of ivette shell wrappers $@ on macOS2024-01-28T09:07:54ZJevin SwevalIssue #2687: Fix Makefile escaping of ivette shell wrappers $@ on macOS<!-- Please use the syntax frama-c/frama-c, else it might close unrelated
public issues
-->
Close pub/frama-c#2687
## Description
Good 'ol make/shell escaping bug fix for issue #2687.
## Companion MRs
No external plug-in impacte...<!-- Please use the syntax frama-c/frama-c, else it might close unrelated
public issues
-->
Close pub/frama-c#2687
## Description
Good 'ol make/shell escaping bug fix for issue #2687.
## Companion MRs
No external plug-in impacted
## Tasks
- [x] API documentation is up-to-date, or no need to update
- [x] Manuals are up-to-date (and the CI manuals target has been run), or no
need to update (including ACSL manual)
- [x] Opam dependencies versions are up-to-date (and CI Opam targets have been
run), or no changes
## Proposed Changelog Entry
Ivette (macOS): Fix launcher script not accepting arguments and erroring out with an errant `\install` arg caused by insufficient Makefile escaping.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/merge_requests/10Update acknowledgement for Roma Maliach-Auguste2023-11-07T03:52:48ZRoma Maliach-AugusteUpdate acknowledgement for Roma Maliach-AugusteHello dear ex-colleagues, I hope you're doing well!
Time flies since I've done my internship at LSL :mask: . Even though I literally couldn't see you a lot, I take advantage of this MR to say again that it was a real pleasure to meet yo...Hello dear ex-colleagues, I hope you're doing well!
Time flies since I've done my internship at LSL :mask: . Even though I literally couldn't see you a lot, I take advantage of this MR to say again that it was a real pleasure to meet you and to work with you (even though the winter of 2020 was really depressing...). I keep a great memory of this internship; all of you were very nice and welcomed me with a lot of kindness and warmth. And I learned a lot. I wish you the best!!
I recently discovered that I was part of the LGBTQIA+ community - the label of "non-binary" suits me. (It means that, in my entire life, I never quite liked being assigned to the gender role of "boy", and being a "girl" does not suit me neither. Each time other people or society tried to make me fit the role of "boy", I was very hurt, internally, even though I did not express it a lot.)
Acknowledging this about me made my life a lot more peaceful. Not easier, because queer people are often targeted by bigots, but anyway, accepting myself and letting others know who I am is, overall, very beneficial for me. That's why I changed my surname to Roma, and that's the identity under which I present myself to new people.
Letting vestiges of my previous surname on the internet is actually harmful for me, because some people without any bad intentions may make a confusion, and ill-intended people may actively try to look for this name, and intentionally use it to hurt me.
During my internship, I made a few minor contributions to this manual, and you duly attributed me, and I thank you for that. But this manual and public; if you could accept this MR, or remove my name in the following editions, I would be grateful.
(ps: as I was a little busy during the last years, I didn't show up, but I was still a subscriber of LSL-misc, and I'm still around Paris, if some of you are still there I may, someday, fill in my name on a framadate and bring nice stuff like chocolate)
Yours,
Romahttps://git.frama-c.com/pub/frama-c/-/merge_requests/9[ivette] fix unintentional macOS argument splitting2023-10-24T19:15:32ZMarvin Häuser[ivette] fix unintentional macOS argument splitting## Description
The macOS launch script for Ivette does not respect the quotation of arguments with spaces. As such, no matter the quotation, arguments are split when encountering spaces. This merge request fixes the launch script to pre...## Description
The macOS launch script for Ivette does not respect the quotation of arguments with spaces. As such, no matter the quotation, arguments are split when encountering spaces. This merge request fixes the launch script to preserve arguments with spaces as a whole.
## Companion MRs
No external plug-in impacted
## Proposed Changelog Entry
`-* Ivette [YYYY-MM-DD] Fixes macOS argument splitting despite quotation.`Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/merge_requests/8Draft: Replace axiomatic lists with standard Why3 lists in WP plugin2023-04-05T07:19:14ZkwaxerDraft: Replace axiomatic lists with standard Why3 lists in WP pluginThis is a follow-up to the [discussion](https://groupes.renater.fr/sympa/arc/frama-c-discuss/2023-01/msg00008.html) from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.
Replaced an axiomatic definition o...This is a follow-up to the [discussion](https://groupes.renater.fr/sympa/arc/frama-c-discuss/2023-01/msg00008.html) from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.
Replaced an axiomatic definition of lists with the standard Why3 one:
- used standard Why3 list modules;
- replaced a declared list type with the standard one;
- provided definitions of all previously specified list functions except for `repeat_box`;
- replaced all axioms with lemmas except for those related to `repeat_box`;
- proved all new lemmas with Alt-Ergo and Isabelle/HOL;
- added Why3 session with Why3 realization files and associated Isabelle/HOL theories.
Facts `nth_cons` and `nth_concat` received a new premise for the index `0 <= k`. All other facts have been kept intact.https://git.frama-c.com/pub/frama-c/-/merge_requests/7Fix/make depend macos2022-07-06T13:04:15ZAndre MaronezeFix/make depend macosAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/merge_requests/5WIP: [Libc] add non-POSIX header sys/sendfile.h + test2021-06-09T12:33:14ZAndre MaronezeWIP: [Libc] add non-POSIX header sys/sendfile.h + testAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/merge_requests/4[tests] use shorter, path-independent includes2021-04-16T11:52:54ZAndre Maroneze[tests] use shorter, path-independent includesAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/merge_requests/3Fixed a semantic error concerning ISO C99 Uninitialized Value Undefined Behav...2020-06-09T14:22:51ZDario PintoFixed a semantic error concerning ISO C99 Uninitialized Value Undefined Behaviour in Eva main manualEn lisant la doc d'Eva, page 19:
"Reading an initialized value is an undefined behavior according to the ISO C99 standard (and can even lead to security vulnerabilities)."
vs
"Reading an **UN**initialized value is an undefined behavio...En lisant la doc d'Eva, page 19:
"Reading an initialized value is an undefined behavior according to the ISO C99 standard (and can even lead to security vulnerabilities)."
vs
"Reading an **UN**initialized value is an undefined behavioraccording to the ISO C99 standard (and can even lead to security vulnerabilities)."Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/merge_requests/2[gitlab] Indicate that the old BTS is deprecated2020-11-28T04:22:07ZAndre Maroneze[gitlab] Indicate that the old BTS is deprecatedFixes #1.Fixes #1.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/merge_requests/1CONTRIBUTING file2021-02-22T13:27:00ZDavid BühlerCONTRIBUTING file