Skip to content

3D test case generation on Windows #177

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
tahina-pro merged 24 commits into from
Mar 19, 2025
Merged

3D test case generation on Windows #177

tahina-pro merged 24 commits into from
Mar 19, 2025

Conversation

@tahina-pro
Copy link
Member

@tahina-pro tahina-pro commented Mar 19, 2025

Other improvements not related to Windows:

  • In test case generation mode (--z3_test or _z3_diff_test), 3D now produces a C test case module by default, testcases.c, even with --no_batch. To avoid producing this test case module, 3D accepts the new option --z3_skip_testcases_c
  • The test case executable now prints the test case definitions as C global variables with everything else commented out
  • Use C11 memset instead of BSD/non-POSIX bzero to initialize outparameters
  • Use NULL instead of zero-sized stack arrays
  • --odir: create output directory if it does not exist

tahina-pro added 24 commits March 19, 2025 11:23
@tahina-pro
on Windows, run z3 sequentially
2e46eff
@tahina-pro
add a z3 test generation test
584f4d9
@tahina-pro
CI: enable z3 test generation test
5572937
@tahina-pro
testgen with fixed elf size
033eb79
@tahina-pro
add 3d option --z3_produce_testcases_c, set by default
0b4887d
@tahina-pro
tests Makefiles: use z3-4.13.3 for test case generation
6bf3566
@tahina-pro
Windows package: download the latest z3 for test case generation
a7706c6
@tahina-pro
from_z3: trim lines (because of Windows line endings)
7d41296
@tahina-pro
package: use curl instead of wget
d161296
@tahina-pro
set executable permissions on Windows
7023031
@tahina-pro
create testcases.c before generating the parser
cb9b0dc
@tahina-pro
do not run make on Windows
d82fdb0
@tahina-pro
do not allocate zero-size stack arrays
44f1b39
@tahina-pro
--odir: create directory if it does not exist
04b9cd0
@tahina-pro
build and run the test executable on Windows
099f01a 
using Karamel's cl-wrapper.bat (cf. FStarLang/karamel#535, thanks @mtzguido !)
@tahina-pro
package: remove .pdb from z3-latest
52d4795
@tahina-pro
parsing failure in error handler printed out as C comment
9d136db
@tahina-pro
bzero -> memset
ef53a55
@tahina-pro
comment out parser call when printing out C witness
9f3998e
@tahina-pro
comment out printed outparameter values
20fd6d7
@tahina-pro
cd out_dir before compiling test.exe on Windows
aca5a7f 
this is necessary because MSVC produces .obj files in the
current directory, and there is no way to change that other than
to switch directory beforehand
@tahina-pro
move printing of newline after outparameters
d340767
@tahina-pro
no_z3_produce_testcases_c -> z3_skip_testcases_c
0bd7bfa
@tahina-pro
Windows CI: test ELFTestGen
b062a4c
@tahina-pro tahina-pro merged commit b59fc46 into master Mar 19, 2025
11 of 12 checks passed
@tahina-pro tahina-pro deleted the _taramana_3d_z3_windows branch March 19, 2025 23:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@tahina-pro