Benjamin Jorge
4b373538ee
Fix API examples
2025-11-24 13:16:22 +01:00
Benjamin Jorge
350cc165aa
Support module with interface in parsing API
2025-11-20 14:24:32 +01:00
Benjamin Jorge
a07a1b6a88
Improve Pmodule API, update documentation
2025-11-20 14:14:24 +01:00
Benjamin Jorge
24523434a3
Fix API examples
2025-11-20 14:14:24 +01:00
Li-yao Xia
5ef8115d8d
Update term to carry multiple locations
2025-10-17 20:23:02 +02:00
MARCHE Claude
ff86d53bf2
Produce special float values in counterexamples
2025-06-11 13:09:37 +02:00
Claude Marche
50f084bf55
Merge branch 'bugfix/v1.8'
2025-06-04 11:10:16 +02:00
Claude Marche
e991d73789
update headers
2025-06-04 10:51:30 +02:00
Jean-Christophe Filliâtre
53b3249062
list.Distinct using a recursive definition
2025-05-14 17:32:28 +02:00
MARCHE Claude
52cc1f8f72
Merge branch 'rac-failure-log-environment' into 'master'
...
Log entire environment at RAC failure
See merge request why3/why3!1200
2025-03-27 08:36:53 +01:00
MARCHE Claude
997bdc53c1
add simple examples of iterators on sets with extraction to OCaml
...
The stdlib is augmented with iterator mechanisms
The OCaml extraction driver is augmented accordingly, using OCaml Seq
2025-03-26 17:20:01 +01:00
Claude Marche
534bd32d04
Do not introduce program variables for zero and one in int.Int module
2025-03-26 15:17:05 +01:00
Claude Marche
82ec599640
restored API example for counterexamples
2025-03-03 13:12:26 +01:00
Matteo Manighetti
9cfa339ada
Adapt counterexample example to check_ce API
2025-02-28 10:46:05 +01:00
Matteo Manighetti
7b3ec0ad7d
Check_ce: simplify API interface
...
All functions in Check_ce now assume that counterexample checking
has been requested. Two entry functions are provided, to request
both small and giant step RAC (useful for checking WhyML programs)
or to only request giant step RAC (useful when the small-step will
be performed on another language).
The RAC log is returned, and should be interpreted to produce a
counterexample. As a temporary helper, an incomplete model is also
returned, that contains all the values extracted from the log.
2025-02-10 18:20:22 +01:00
Guillaume Melquiond
8a86d9ac62
Update copyright years.
2024-12-07 09:01:55 +01:00
Claude Marche
27524abdc9
improved Ptree helpers
2024-10-30 19:38:19 +01:00
Matteo Manighetti
4ef9300722
Disable completely prepare_for_counterexamples
2024-10-11 13:30:51 +02:00
MARCHE Claude
a74598f928
do not take resource limits from more than one source
2024-10-08 21:00:00 +02:00
MARCHE Claude
25a128513d
drivers for Alt-Ergo 2.6: FPA implicit, CE and BV
2024-10-08 15:11:12 +02:00
Matteo Manighetti
7f1c78a541
Simplify option for printing JSON counterexamples
2024-09-18 10:43:15 +02:00
Loïc Correnson
e2afddb11d
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
Paul Bonnot
9062fa94e0
Add function to get the list of calls and loops
...
Change the display of subcontrat weakness
WIP
Detect stdlib rs by path
Now rs filtering seems ok
restore previous output messages, to avoid tons of changes
restore previous output messages, to avoid tons of changes, more
Deleted mlw_builtin_attr
Better display
Updated oracles
Oracles OK now !
2023-10-11 15:47:30 +02:00
BONNOT Paul
29c71dbd51
add a meta to mark a symbol as never removed by remove_unused*
...
mark some lemmas on division of real as removable if not needed
2023-06-15 15:18:48 +00:00
BONNOT Paul
f0b1e61df5
Add an option to allow hiding uses, clones and metas in printed tasks
2023-05-26 12:16:30 +00:00
