Skip to content

Commit

Permalink
feature: implement @old with local variables thus expression types ar…
Browse files Browse the repository at this point in the history
…e handled by GO
  • Loading branch information
chavacava committed Jan 1, 2025
1 parent ebc6a66 commit a8654ae
Showing 1 changed file with 10 additions and 9 deletions.
19 changes: 10 additions & 9 deletions internal/contract/generator/generator.go
Original file line number Diff line number Diff line change
Expand Up @@ -361,31 +361,32 @@ func (fileAnalyzer) generateLetCode(let contract.Let) (r string) {
// @requires clauses != nil && len(clauses) > 0
// @ensures r != ""
func (fa fileAnalyzer) generateEnsuresCode(clauses []contract.Ensures, fd *ast.FuncDecl) (r string) {
const templateOldVarDecl = commentPrefix + `%oldId% := %expr%`
const templateEnsure = commentPrefix + `if %shortStmt%!(%cond%) { panic("%contract% not satisfied") }`

ensuresCode := make([]string, len(clauses))
funcParams := []string{}
funcArgs := []string{}
oldVarDecls := []string{}
//funcArgs := []string{}
for _, clause := range clauses {
shortStmt, expr, idToOld := clause.ExpandedExpression()
if shortStmt != "" {
shortStmt = shortStmt + "; "
}
for id, old := range idToOld {
funcParams = append(funcParams, fmt.Sprintf("%s %s", old, fa.getTypeForID(id, fd)))
funcArgs = append(funcArgs, id)
for expr, oldId := range idToOld {
decl := strings.Replace(templateOldVarDecl, "%oldId%", oldId, 1)
decl = strings.Replace(decl, "%expr%", expr, 1)
oldVarDecls = append(oldVarDecls, decl)
}
ensure := strings.Replace(templateEnsure, "%shortStmt%", shortStmt, 1)
ensure = strings.Replace(ensure, "%cond%", expr, 1)
ensure = strings.Replace(ensure, "%contract%", escapeDoubleQuotes(clause.String()), 1)
ensuresCode = append(ensuresCode, ensure)
}

const templateDeferredFunction = commentPrefix + `defer func(%params%){%checks%}(%args%)`
r += strings.Join(oldVarDecls, "\n")

r = strings.Replace(templateDeferredFunction, "%params%", strings.Join(funcParams, ","), 1)
r = strings.Replace(r, "%checks%", strings.Join(ensuresCode, "\n"), 1)
r = strings.Replace(r, "%args%", strings.Join(funcArgs, ","), 1)
const templateDeferredFunction = commentPrefix + "\ndefer func(){%checks%}()"
r += strings.Replace(templateDeferredFunction, "%checks%", strings.Join(ensuresCode, "\n"), 1)

return r
}
Expand Down

0 comments on commit a8654ae

Please sign in to comment.