* main.go, transform/debug.go,
transform/unroll_loop.go: Here.

* main.go, transform/waitgroup.go,
transform/meta.go: Here.

* main.go: Here.

* main.go: Here.

* main.go: Here.

* main.go: Here.

Hugo Moreau authored 3 years ago and Etienne Renault committed 3 years ago

Blackbox can now handle global array.

 * main.go : Here.

Hugo Moreau authored 3 years ago and Etienne Renault committed 3 years ago

If blackbox is set to auto, the blackbox functions are defined with the
formula.

 * main.go,
   tools/formulae.go : Here.

Hugo Moreau authored 3 years ago and Etienne Renault committed 3 years ago

Go2Pins now accepts a second argument, a formula to run directly
modelchecking on it.

 * main.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

By calling go2pins with rers, it will automatically detect the RERS
input values.

 * benchs/run-blackbox/test.sh,
   main.go,
   tools/rers.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

In order to make easier the use of blackbox, for a given file, if we
pass a formulae file to go2pins, it will automatically set the functions
to be blackboxed.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

In order to avoid conflict with global variables defined after assigning
to it, LocalVariableAssignments has been corrected.

 * main.go,
   transform/localvariableassignments.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

Handling multiple func call as assignments by creating a tmp variables.

 * main.go,
   transform/innercall.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

 * main.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

 * main.go,
   tools/blackbox.go,
   transform/global.go,
   transform/postglobal.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

The blackbox package now import structs only if the blackboxed contains
global variables, it was importing it everytime before.

 * main.go,
   transform/blackbox.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

Blackboxed functions are now able to handle global variables, by using
G2PState as a reference.

 * main.go,
   tools/blackbox.go,
   transform/checktype.go, transform/global.go,
   transform/globaltostate.go, transform/localvariableassignments.go,
   transform/postglobal.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

For future global variable access via `Blackbox`, all type generated by
Go2Pins are now stored in a dedicated package `structs`.
All convenient modifications has been done to let Go2Pins in a valid
state.

 * boilerplate/Makefile, boilerplate/main.go,
   boilerplate/structs/structs.go,
   decl/decl.go,
   main.go,
   tools/blackbox.go,
   transform/meta.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

Global var can be placed in all the file and not necessarily before its
actual using. So it is now detected before applying the transform.

 * main.go,
   transform/global.go,
   transform/preglobal.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

In order to have a cleaner code and a better readibility, code has been
refactored and documented. It has been explicit name accordingly on
the moment it is summoned.
transform/global.go now handle both Getter and Setter configuration.
transform/postglobal.go handle injecting Getter and Setter definition in
ast.

 * main.go,
   transform/global.go,
   transform/postglobal.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

 * main.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

For a better readibility, better format has been used for formating.

 * main.go,
   tools/formating.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

 * main.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

To avoid trouble during transform, setter are done first, then getter.

 * main.go,
   transform/global.go,
   transform/global2.go,
   transform/global3.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

 * main.go

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

For now, only regular assignment was handled.

 * main.go,
   transform/global.go, transform/global2.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

Global are now identified and not mixed with local variables.
funcptr are used to set their values.

 * main.go,
   tests/global.go,
   transform/global.go
   transfrom/global2.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

Global variables are now modified funcptr,
still need to create the functions.

 * main.go,
   tests/global.go,
   transform/global.go : Here.

Hugo Moreau authored 4 years ago and Etienne Renault committed 3 years ago

Setting up basis for the transform.

 * main.go, transform/global.go : Here.

 * boilerplate/Makefile,
   main.go, tools/blackbox.go : Here.

Typing "make -C output" is now obsolete

* boilerplate/main.go,
main.go: Here.

* main.go,
tools/blackbox.go,
tools/callgraph.go,
tools/extract_blackboxes/main.go,
tools/recursion.go: Here.

* main.go: Here.

* .last-cl-gen, ChangeLog, NEWS.txt, main.go: Here.

* main.go, transform/debug.go: Here.

* Rename transform/arraytreatment.go
to transform/desugararray.go: Here.

* main.go: Here.

* main.go, tests/concurrent_fibonacci.go: Here.

* main.go: Here.

Note that even if channels are fully supported
by the scheduler, some syntax declaration element
are not supported

* boilerplate/main.go,
cspinfo/channel.go,
decl/decl.go,
main.go,
tests/prod_cons_simp.go,
transform/afterchannels.go,
transform/channels.go,
transform/meta.go: Here.