1. 21 Jan, 2020 12 commits
    • Etienne Renault's avatar
      Blackbox and global variables are not supported. · 152a00a4
      Etienne Renault authored
      If a Blackbox (BB) function modifies variable that is also used inside
      of a non-blackbox function the following problem occurs: the variable
      cannot be neither in the blackbox package neither in the normal
      package.
      
      We should try to resolve this problem by :
         (1) analysis wether variables are exclusively used by BB-fun
         (2) pass setter as additionnal argument to BB-functions
      
      Still for now it is preferable to forbbids BB and globals.
      
      * main.go, transform/checktype.go: Here.
      152a00a4
    • Etienne Renault's avatar
      Add RERS benchmark · 50468710
      Etienne Renault authored
      * benchs/RERS/2016-Problem10.go,
      benchs/RERS/2016-Problem11.go,
      benchs/RERS/2016-Problem12.go,
      benchs/RERS/2016-Problem14.go,
      benchs/RERS/2016-Problem15.go,
      benchs/RERS/2017-Problem10.go,
      benchs/RERS/2017-Problem11.go,
      benchs/RERS/2017-Problem12.go,
      benchs/RERS/2017-Problem14.go,
      benchs/RERS/2017-Problem15.go,
      benchs/RERS/2018-Problem10.go,
      benchs/RERS/2018-Problem11.go,
      benchs/RERS/2019-Problem11.go,
      benchs/RERS/2019-Problem12.go,
      benchs/RERS/2019-Problem14.go,
      benchs/RERS/2019-Problem15.go,
      benchs/RERS/rers2go.sh,
      benchs/run-benchmark.sh: Here.
      50468710
    • Etienne Renault's avatar
      Restricted support for closures encountered in RERS · ef351ebe
      Etienne Renault authored
      Thanks to A. Martin for this patch
      
      * transform/functiondefs.go: here.
      ef351ebe
    • Etienne Renault's avatar
      Bug fix when -rers option is not available · 894a07f1
      Etienne Renault authored
      * boilerplate/main.go, main.go: Here.
      894a07f1
    • Etienne Renault's avatar
      Avoid parsing errors for options · 710ca455
      Etienne Renault authored
      * main.go: Here.
      710ca455
    • Etienne Renault's avatar
      Add support for RERS. · 4c4096bd
      Etienne Renault authored
      In RERS challenges, file are written in C and
      the environment is modelled by scanf("%d",...).
      
      During the translation, this statement has been
      converted into __RERS__ = __RERS__ + 1, since this
      variable is only used to represents the environment.
      
      As a consequence, the option -rers "1;2;3" will modify
      the previous assignment in order to represent the
      environment. In other this instruction will be replaced
      by three assignment
         - __RERS__ = 1
         - __RERS__ = 2
         - __RERS__ = 3
      while  the instruction __RERS__ = __RERS__ + 1 will be discarded
      
      * boilerplate/main.go, main.go: Here.
      4c4096bd
    • Etienne Renault's avatar
      blackbox: conditionnal warning · f530cfc3
      Etienne Renault authored
      * tools/blackbox.go: here.
      f530cfc3
    • Etienne Renault's avatar
      Output warning when automatic blackboxing functions · d07f8d80
      Etienne Renault authored
      * tools/blackbox.go: Here.
      d07f8d80
    • Etienne Renault's avatar
      Fix typo during rewritting · 57f06d5a
      Etienne Renault authored
      * tools/blackbox.go: here.
      57f06d5a
    • Etienne Renault's avatar
      Fix bug when goroutines but no channels · 9d897a2f
      Etienne Renault authored
      *  boilerplate/main.go: Here.
      9d897a2f
    • hmoreau's avatar
      Test for channel · 0d5e8dfc
      hmoreau authored
      * tests/prod_cons_simp.go: Here.
      0d5e8dfc
    • hmoreau's avatar
      Generate successors for channels · 1db6bf82
      hmoreau authored
      * boilerplate/main.go,
        channel/channel.go,
        decl/decl.go,
        main.go,
        transform/afterchannels.go,
        transform/channels.go: Here.
      1db6bf82
  2. 20 Jan, 2020 1 commit
  3. 17 Jan, 2020 4 commits
    • hmoreau's avatar
      Array are supported · b42012d0
      hmoreau authored
      Removing useless pass for testing if array are used or not
      
      * tests/passes/array.go,
        transform/checktype.go: Here.
      b42012d0
    • hmoreau's avatar
      New channel package created · 8f3889b9
      hmoreau authored
      In order to recover more easily where the channels are set up, a new
      package has been created, giving details about it.
      
      * boilerplate/main.go,
        channel/channel.go,
        decl/decl.go,
        main.go: Here.
      8f3889b9
    • hmoreau's avatar
      Channel treatment integrated to compileTo · 734cfb2d
      hmoreau authored
      Channels are now treated with all the other transform
      
      * main.go,
        transform/channels.go: Here.
      734cfb2d
    • hmoreau's avatar
      Tmp variables for UnaryExpr used in CallExpr · 03d23ee7
      hmoreau authored
      For a better translations and uses of channels, when they are used in
      function calls, temporary variables are created.
      
      * transform/channels.go: Here.
      03d23ee7
  4. 14 Jan, 2020 1 commit
  5. 13 Jan, 2020 4 commits
  6. 18 Dec, 2019 5 commits
  7. 13 Dec, 2019 3 commits
    • hmoreau's avatar
      New struct for better implem of channel · 98ebca52
      hmoreau authored
      In order to facilitate channel transformation process, a new struct has
      been created `chanInfo` :
      
      ```
      type chanInfo struct {
          local, global string
          index         int
      }
      ```
      
      With this, we can easily find the original name of the channel if it is
      different in the function. The index indicates where the function is
      in the array of states and values.
      
      * transform/channels.go: Here.
      98ebca52
    • hmoreau's avatar
      48808e3b
    • Etienne Renault's avatar
      ltsmin: abi has changed · 6dd64e1b
      Etienne Renault authored
      This patch provide a support for LTSmin
      except for partial order reductions.
      
      * boilerplate/go2pins.c,
      boilerplate/go2pins.h,
      boilerplate/main.go: here.
      6dd64e1b
  8. 12 Dec, 2019 2 commits
  9. 11 Dec, 2019 2 commits
  10. 09 Dec, 2019 3 commits
  11. 04 Dec, 2019 1 commit
  12. 03 Dec, 2019 1 commit
  13. 29 Nov, 2019 1 commit
    • hmoreau's avatar
      Displays channel information · 0f24fee3
      hmoreau authored
      use `./go2pins -chaninfo <file>` to display channel information
      
      * main.go,
        transform/channels.go: Here.
      0f24fee3