Commit bc162002 authored by Etienne Renault's avatar Etienne Renault

support multiple explicit variable declaration

Commit 211baa6d simplifies the way `alive`
variables are handled. Nonethless it introduces
a bug when multiple explicit variable declaration
occur in the same line. This commit fixes that.

* tests/expected, tests/multiple.go,
tests/run.sh, transform/normalizedeclarations.go: Here.
parent b2162945
......@@ -8,4 +8,5 @@
#fibonacci.go,43,43
#if.go,13,13
#mywhile.go,255,255
#multiple.go,6,6
#prod_cons_simp.go,44,74
// Copyright (C) 2020 Laboratoire de Recherche et Developpement
// de l'EPITA (LRDE).
//
// This file is part of Go2Pins, a tool for Golang model-checking
//
// Go2Pins is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Go2Pins is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
package main
func main() {
var v1 int = 1
var (
v2 int = 1
v3 = 2
)
v1 = v2 + v3 + v1
}
......@@ -31,7 +31,6 @@ for i in $(ls *.go); do
../go2pins -f -o output $i > /dev/null 2>&1
cd output > /dev/null 2>&1
make > /dev/null 2>&1
./go2pins-mc -kripke-size
TMP=$(./go2pins-mc -kripke-size | grep '#' | sed "s/kripke/$i/g")
EXPECTED=$(cat ../expected | grep "#$i,")
RES=$(diff <(echo "$TMP") <(echo "$EXPECTED"))
......
......@@ -65,32 +65,35 @@ func (t *NormalizeDeclarations) Pre(meta *Meta, v *Visitor) bool {
t.stmtList = nil
}
case *ast.ValueSpec:
if t.stmtList != nil {
newLHS := make([]ast.Expr, 0)
newLHS = append(newLHS, node.Names[0])
if node.Values == nil {
t.stmtList.List[t.stmtIndex] = &ast.AssignStmt{
Lhs: newLHS,
// Replace declarations by type inference assignments
Tok: token.DEFINE,
Rhs: []ast.Expr{
&ast.BasicLit{
Kind: token.INT,
Value: "0",
},
},
}
} else {
t.stmtList.List[t.stmtIndex] = &ast.AssignStmt{
Lhs: newLHS,
// Replace declarations by type inference assignments
Tok: token.DEFINE,
Rhs: node.Values,
if t.stmtList == nil {
return true
}
newLHS := make([]ast.Expr, 0)
newRHS := make([]ast.Expr, 0)
for i, _ := range node.Specs {
switch vs := node.Specs[i].(type) {
case *ast.ValueSpec:
newLHS = append(newLHS, vs.Names[0])
if vs.Values == nil {
newRHS = append(newRHS, &ast.BasicLit{
Kind: token.INT,
Value: "0",
})
} else {
newRHS = append(newRHS, vs.Values[0])
}
}
}
t.stmtList.List[t.stmtIndex] = &ast.AssignStmt{
Lhs: newLHS,
// Replace declarations by type inference assignments
Tok: token.DEFINE,
Rhs: newRHS,
}
}
return true
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment