diff --git a/Makefile b/Makefile index 50c7112..01acfbf 100755 --- a/Makefile +++ b/Makefile @@ -48,7 +48,7 @@ OBJS = ImpMain.o ImpParser.o ImpTypeChecker.o ImpFormula.o ImpAST.o \ .y.hs: happy -agci $< -all: imp fixcalc +all: imp fixcalc loopinv imp : $(OBJS) ImpParser.y ImpMain.hs rm -f $@ @@ -58,6 +58,7 @@ imp : $(OBJS) ImpParser.y ImpMain.hs clean: rm -f *.hi *.o *~ imp ImpParser.hs *.info a.omega a.all.c a.c a.out a.impi a.impt a.omega-err a.pre oc.out fixcalc FixCalcParser.hs log + rm -f loopinv-bin $(LOOPINV_DIR)/*.hi $(LOOPINV_DIR)/*.o install: fixcalc scp fixcalc popeeaco@loris-7.ddns:/home/popeeaco/bin/. @@ -77,6 +78,23 @@ fixcalc: $(FixCalcOBJS) FixCalcParser.y FixCalcMain.hs ghc -o fixcalc $(HC_OPTS) -lstdc++ FixCalcMain.hs $(LIBS) $(OMEGA_LIBS) $(RAZVAN_LIBS) ##### +##### LoopInv - Loop Invariant Generator +LOOPINV_DIR = loopinv +LOOPINV_SRCS = $(LOOPINV_DIR)/AST.hs $(LOOPINV_DIR)/Lexer.hs \ + $(LOOPINV_DIR)/Parser.hs $(LOOPINV_DIR)/ImpEmit.hs \ + $(LOOPINV_DIR)/Main.hs + +loopinv: $(LOOPINV_SRCS) imp + ghc -o loopinv-bin -i$(LOOPINV_DIR) -package process -package filepath \ + --make $(LOOPINV_DIR)/Main.hs + +loopinv-test: loopinv + cd $(LOOPINV_DIR)/examples && ../../loopinv-bin test1.c + +loopinv-clean: + rm -f loopinv-bin $(LOOPINV_DIR)/*.hi $(LOOPINV_DIR)/*.o +##### + static: $(FixCalcOBJS) FixCalcParser.y FixCalcMain.hs rm -f fixcalc ghc -o fixcalc $(HC_SOPTS) -lstdc++ FixCalcMain.hs $(LIBS) $(OMEGA_LIBS) $(RAZVAN_LIBS) diff --git a/loopinv/AST.hs b/loopinv/AST.hs new file mode 100644 index 0000000..e31d386 --- /dev/null +++ b/loopinv/AST.hs @@ -0,0 +1,52 @@ +-- | Simple AST for C subset (loops, assignments, basic expressions) +module AST where + +-- | A program is a list of functions +data Program = Program [Func] + deriving (Show, Eq) + +-- | Function definition +data Func = Func { + funcRetType :: Type, + funcName :: String, + funcParams :: [(Type, String)], + funcBody :: [Stmt] + } + deriving (Show, Eq) + +-- | Types we support +data Type = TInt | TVoid + deriving (Show, Eq) + +-- | Statements +data Stmt + = VarDecl Type String (Maybe Expr) -- int x = 0; + | Assign String Expr -- x = expr; + | While Expr [Stmt] -- while (cond) { body } + | If Expr [Stmt] (Maybe [Stmt]) -- if (cond) { } else { } + | Return (Maybe Expr) -- return expr; + | ExprStmt Expr -- expr; + deriving (Show, Eq) + +-- | Expressions +data Expr + = Var String -- variable + | Lit Int -- integer literal + | BinOp BinOp Expr Expr -- e1 op e2 + | UnaryOp UnaryOp Expr -- op e + | Call String [Expr] -- func(args) + deriving (Show, Eq) + +-- | Binary operators +data BinOp + = Add | Sub | Mul | Div | Mod -- arithmetic + | Lt | Le | Gt | Ge | Eq | Ne -- comparison + | And | Or -- logical + deriving (Show, Eq) + +-- | Unary operators +data UnaryOp = Neg | Not + deriving (Show, Eq) + + + diff --git a/loopinv/ImpEmit.hs b/loopinv/ImpEmit.hs new file mode 100644 index 0000000..3ac9301 --- /dev/null +++ b/loopinv/ImpEmit.hs @@ -0,0 +1,115 @@ +-- | Emit AST as Imp language syntax +module ImpEmit (emitImp) where + +import AST +import Data.List (intercalate) + +-- | Convert program to Imp source code +emitImp :: Program -> String +emitImp (Program funcs) = + "#include \"Primitives.imp\"\n\n" ++ + intercalate "\n\n" (map emitFunc funcs) + +-- | Emit a function +emitFunc :: Func -> String +emitFunc (Func retType name params body) = + emitType retType ++ " " ++ name ++ "(" ++ emitParams params ++ ") {\n" ++ + emitStmts 1 body ++ + "}" + +-- | Emit type +emitType :: Type -> String +emitType TInt = "int" +emitType TVoid = "void" + +-- | Emit parameters +emitParams :: [(Type, String)] -> String +emitParams = intercalate ", " . map (\(t, n) -> emitType t ++ " " ++ n) + +-- | Emit statements with indentation +emitStmts :: Int -> [Stmt] -> String +emitStmts indent stmts = + concatMap (emitStmt indent) (init' stmts) ++ + emitStmtLast indent (last' stmts) + where + -- All statements except last get semicolon + init' [] = [] + init' xs = init xs + -- Last statement has no trailing semicolon (Imp uses ; as separator) + last' [] = Nothing + last' xs = Just (last xs) + +-- | Emit a statement (not the last one - includes semicolon separator) +emitStmt :: Int -> Stmt -> String +emitStmt indent stmt = emitStmtCore indent stmt ++ ";\n" + +-- | Emit the last statement (no semicolon) +emitStmtLast :: Int -> Maybe Stmt -> String +emitStmtLast _ Nothing = "" +emitStmtLast indent (Just stmt) = emitStmtCore indent stmt ++ "\n" + +-- | Emit statement core (without semicolon) +emitStmtCore :: Int -> Stmt -> String +emitStmtCore indent stmt = + let ind = replicate (indent * 2) ' ' + in case stmt of + VarDecl typ name Nothing -> + ind ++ emitType typ ++ " " ++ name ++ " := 0" -- Imp needs initialization + VarDecl typ name (Just expr) -> + ind ++ emitType typ ++ " " ++ name ++ " := " ++ emitExpr expr + Assign name expr -> + ind ++ name ++ " := " ++ emitExpr expr + While cond body -> + ind ++ "while (" ++ emitExpr cond ++ ") do {\n" ++ + emitStmts (indent + 1) body ++ + ind ++ "}" + If cond thenBody Nothing -> + ind ++ "if " ++ emitExpr cond ++ " then {\n" ++ + emitStmts (indent + 1) thenBody ++ + ind ++ "} else { Void }" + If cond thenBody (Just elseBody) -> + ind ++ "if " ++ emitExpr cond ++ " then {\n" ++ + emitStmts (indent + 1) thenBody ++ + ind ++ "} else {\n" ++ + emitStmts (indent + 1) elseBody ++ + ind ++ "}" + Return Nothing -> + ind ++ "Void" + Return (Just expr) -> + ind ++ emitExpr expr + ExprStmt expr -> + ind ++ emitExpr expr + +-- | Emit expression +emitExpr :: Expr -> String +emitExpr (Var name) = name +emitExpr (Lit n) = show n +emitExpr (BinOp op e1 e2) = + "(" ++ emitExpr e1 ++ " " ++ emitBinOp op ++ " " ++ emitExpr e2 ++ ")" +emitExpr (UnaryOp op e) = emitUnaryOp op ++ emitExpr e +emitExpr (Call name args) = + name ++ "(" ++ intercalate ", " (map emitExpr args) ++ ")" + +-- | Emit binary operator +emitBinOp :: BinOp -> String +emitBinOp Add = "+" +emitBinOp Sub = "-" +emitBinOp Mul = "*" +emitBinOp Div = "/" +emitBinOp Mod = "%" +emitBinOp Lt = "<" +emitBinOp Le = "<=" +emitBinOp Gt = ">" +emitBinOp Ge = ">=" +emitBinOp Eq = "=" -- Imp uses = for equality in expressions +emitBinOp Ne = "<>" -- Imp uses <> for not equal +emitBinOp And = "&&" +emitBinOp Or = "||" + +-- | Emit unary operator +emitUnaryOp :: UnaryOp -> String +emitUnaryOp Neg = "-" +emitUnaryOp Not = "!" + + + diff --git a/loopinv/Lexer.hs b/loopinv/Lexer.hs new file mode 100644 index 0000000..f06f0ac --- /dev/null +++ b/loopinv/Lexer.hs @@ -0,0 +1,85 @@ +-- | Simple lexer for C subset +module Lexer (Token(..), tokenize) where + +import Data.Char (isAlpha, isAlphaNum, isDigit, isSpace) + +-- | Tokens +data Token + = TkInt | TkVoid -- types + | TkWhile | TkIf | TkElse | TkReturn -- keywords + | TkIdent String -- identifier + | TkNum Int -- number + | TkPlus | TkMinus | TkStar | TkSlash | TkPercent -- arithmetic + | TkLt | TkLe | TkGt | TkGe | TkEqEq | TkNe -- comparison + | TkAnd | TkOr | TkNot -- logical + | TkAssign -- = + | TkLParen | TkRParen -- ( ) + | TkLBrace | TkRBrace -- { } + | TkSemi | TkComma -- ; , + | TkEOF + deriving (Show, Eq) + +-- | Tokenize a string +tokenize :: String -> [Token] +tokenize [] = [TkEOF] +tokenize s@(c:cs) + | isSpace c = tokenize cs + -- Skip single-line comments + | take 2 s == "//" = tokenize (dropWhile (/= '\n') s) + -- Skip multi-line comments + | take 2 s == "/*" = tokenize (skipBlockComment (drop 2 s)) + -- Two-character operators + | take 2 s == "<=" = TkLe : tokenize (drop 2 s) + | take 2 s == ">=" = TkGe : tokenize (drop 2 s) + | take 2 s == "==" = TkEqEq : tokenize (drop 2 s) + | take 2 s == "!=" = TkNe : tokenize (drop 2 s) + | take 2 s == "&&" = TkAnd : tokenize (drop 2 s) + | take 2 s == "||" = TkOr : tokenize (drop 2 s) + -- Single-character operators + | c == '+' = TkPlus : tokenize cs + | c == '-' = TkMinus : tokenize cs + | c == '*' = TkStar : tokenize cs + | c == '/' = TkSlash : tokenize cs + | c == '%' = TkPercent : tokenize cs + | c == '<' = TkLt : tokenize cs + | c == '>' = TkGt : tokenize cs + | c == '=' = TkAssign : tokenize cs + | c == '!' = TkNot : tokenize cs + | c == '(' = TkLParen : tokenize cs + | c == ')' = TkRParen : tokenize cs + | c == '{' = TkLBrace : tokenize cs + | c == '}' = TkRBrace : tokenize cs + | c == ';' = TkSemi : tokenize cs + | c == ',' = TkComma : tokenize cs + -- Numbers + | isDigit c = let (num, rest) = span isDigit s + in TkNum (read num) : tokenize rest + -- Identifiers and keywords + | isAlpha c || c == '_' = + let (ident, rest) = span isIdentChar s + in keywordOrIdent ident : tokenize rest + | otherwise = error $ "Unexpected character: " ++ [c] + +-- | Check if character can be part of identifier +isIdentChar :: Char -> Bool +isIdentChar c = isAlphaNum c || c == '_' + +-- | Convert identifier to keyword or keep as identifier +keywordOrIdent :: String -> Token +keywordOrIdent "int" = TkInt +keywordOrIdent "void" = TkVoid +keywordOrIdent "while" = TkWhile +keywordOrIdent "if" = TkIf +keywordOrIdent "else" = TkElse +keywordOrIdent "return" = TkReturn +keywordOrIdent s = TkIdent s + +-- | Skip block comment (find closing */) +skipBlockComment :: String -> String +skipBlockComment [] = [] +skipBlockComment s + | take 2 s == "*/" = drop 2 s + | otherwise = skipBlockComment (tail s) + + + diff --git a/loopinv/Main.hs b/loopinv/Main.hs new file mode 100644 index 0000000..a22187d --- /dev/null +++ b/loopinv/Main.hs @@ -0,0 +1,86 @@ +-- | LoopInv: Build constraint abstractions and compute loop invariants via LFP +-- +-- This tool: +-- 1. Converts C code to Imp syntax (constraint abstraction) +-- 2. Runs the imp tool which uses fixCalc to compute LFP +-- 3. Shows the result +-- +module Main where + +import System.Environment (getArgs) +import System.Process (readProcessWithExitCode) +import System.Exit (ExitCode(..)) +import System.FilePath (takeBaseName, takeDirectory, ()) + +import Lexer (tokenize) +import Parser (parse) +import ImpEmit (emitImp) + +main :: IO () +main = do + args <- getArgs + case args of + [inputFile] -> processFile inputFile + _ -> showHelp + +showHelp :: IO () +showHelp = do + putStrLn "LoopInv - Loop Invariant Generator using fixCalc" + putStrLn "" + putStrLn "Usage: loopinv " + putStrLn "" + putStrLn "This tool:" + putStrLn " 1. Converts C code to Imp (constraint abstraction)" + putStrLn " 2. Runs imp tool to compute loop invariants via LFP (fixCalc)" + putStrLn " 3. Displays the computed result" + +processFile :: FilePath -> IO () +processFile inputFile = do + putStrLn "================================================================" + putStrLn " LoopInv - Constraint Abstraction & LFP Computation" + putStrLn "================================================================" + putStrLn "" + + -- Step 1: Read and parse C code + putStrLn $ "Input: " ++ inputFile + putStrLn "" + cCode <- readFile inputFile + + putStrLn "=== Original C Code ===" + putStrLn cCode + + -- Step 2: Convert to Imp (constraint abstraction) + putStrLn "=== Converting to Imp (Constraint Abstraction) ===" + let tokens = tokenize cCode + let ast = parse tokens + let impCode = emitImp ast + + let impFile = takeDirectory inputFile takeBaseName inputFile ++ ".imp" + writeFile impFile impCode + putStrLn $ "Generated: " ++ impFile + putStrLn "" + putStrLn impCode + + -- Step 3: Run imp tool (which calls fixCalc for LFP) + putStrLn "=== Running imp tool (LFP computation via fixCalc) ===" + putStrLn "" + + let impBin = "./imp" + (exitCode, stdout, stderr) <- readProcessWithExitCode impBin [impFile, "+infer"] "" + + case exitCode of + ExitSuccess -> do + putStrLn stdout + + -- Show the LFP result + putStrLn "=== LFP Result (a.impt) ===" + putStrLn "" + imptContent <- readFile "a.impt" + putStrLn imptContent + + ExitFailure code -> do + putStrLn $ "Error: imp tool failed with code " ++ show code + putStrLn "stderr:" + putStrLn stderr + putStrLn "stdout:" + putStrLn stdout diff --git a/loopinv/Parser.hs b/loopinv/Parser.hs new file mode 100644 index 0000000..5919612 --- /dev/null +++ b/loopinv/Parser.hs @@ -0,0 +1,228 @@ +-- | Simple recursive descent parser for C subset +module Parser (parse) where + +import AST +import Lexer + +-- | Parse tokens into a program +parse :: [Token] -> Program +parse toks = Program (parseFuncs toks) + +-- | Parse list of functions +parseFuncs :: [Token] -> [Func] +parseFuncs [TkEOF] = [] +parseFuncs toks = + let (func, rest) = parseFunc toks + in func : parseFuncs rest + +-- | Parse a single function +parseFunc :: [Token] -> (Func, [Token]) +parseFunc toks = + let (retType, toks1) = parseType toks + (name, toks2) = parseIdent toks1 + toks3 = expect TkLParen toks2 + (params, toks4) = parseParams toks3 + toks5 = expect TkRParen toks4 + toks6 = expect TkLBrace toks5 + (body, toks7) = parseStmts toks6 + toks8 = expect TkRBrace toks7 + in (Func retType name params body, toks8) + +-- | Parse type +parseType :: [Token] -> (Type, [Token]) +parseType (TkInt : rest) = (TInt, rest) +parseType (TkVoid : rest) = (TVoid, rest) +parseType toks = error $ "Expected type, got: " ++ show (take 3 toks) + +-- | Parse identifier +parseIdent :: [Token] -> (String, [Token]) +parseIdent (TkIdent s : rest) = (s, rest) +parseIdent toks = error $ "Expected identifier, got: " ++ show (take 3 toks) + +-- | Parse parameters +parseParams :: [Token] -> ([(Type, String)], [Token]) +parseParams (TkRParen : _) = ([], TkRParen : drop 0 []) -- empty params, put back RParen +parseParams toks = parseParams' toks + where + parseParams' ts = + let (typ, ts1) = parseType ts + (name, ts2) = parseIdent ts1 + in case ts2 of + (TkComma : ts3) -> + let (rest, ts4) = parseParams' ts3 + in ((typ, name) : rest, ts4) + _ -> ([(typ, name)], ts2) + +-- | Parse list of statements until } +parseStmts :: [Token] -> ([Stmt], [Token]) +parseStmts (TkRBrace : rest) = ([], TkRBrace : rest) -- put back RBrace +parseStmts toks = + let (stmt, rest) = parseStmt toks + (stmts, rest') = parseStmts rest + in (stmt : stmts, rest') + +-- | Parse a single statement +parseStmt :: [Token] -> (Stmt, [Token]) +-- Variable declaration: int x = expr; or int x; +parseStmt (TkInt : TkIdent name : TkAssign : rest) = + let (expr, rest') = parseExpr rest + rest'' = expect TkSemi rest' + in (VarDecl TInt name (Just expr), rest'') +parseStmt (TkInt : TkIdent name : TkSemi : rest) = + (VarDecl TInt name Nothing, rest) +-- While loop +parseStmt (TkWhile : TkLParen : rest) = + let (cond, rest') = parseExpr rest + rest'' = expect TkRParen rest' + rest''' = expect TkLBrace rest'' + (body, rest4) = parseStmts rest''' + rest5 = expect TkRBrace rest4 + in (While cond body, rest5) +-- If statement +parseStmt (TkIf : TkLParen : rest) = + let (cond, rest') = parseExpr rest + rest'' = expect TkRParen rest' + rest''' = expect TkLBrace rest'' + (thenBody, rest4) = parseStmts rest''' + rest5 = expect TkRBrace rest4 + in case rest5 of + (TkElse : TkLBrace : rest6) -> + let (elseBody, rest7) = parseStmts rest6 + rest8 = expect TkRBrace rest7 + in (If cond thenBody (Just elseBody), rest8) + _ -> (If cond thenBody Nothing, rest5) +-- Return statement +parseStmt (TkReturn : TkSemi : rest) = + (Return Nothing, rest) +parseStmt (TkReturn : rest) = + let (expr, rest') = parseExpr rest + rest'' = expect TkSemi rest' + in (Return (Just expr), rest'') +-- Assignment: x = expr; +parseStmt (TkIdent name : TkAssign : rest) = + let (expr, rest') = parseExpr rest + rest'' = expect TkSemi rest' + in (Assign name expr, rest'') +-- Expression statement +parseStmt toks = + let (expr, rest) = parseExpr toks + rest' = expect TkSemi rest + in (ExprStmt expr, rest') + +-- | Parse expression (with precedence) +parseExpr :: [Token] -> (Expr, [Token]) +parseExpr = parseOr + +-- | Parse || (lowest precedence) +parseOr :: [Token] -> (Expr, [Token]) +parseOr toks = + let (left, rest) = parseAnd toks + in parseOr' left rest + where + parseOr' left (TkOr : rest) = + let (right, rest') = parseAnd rest + in parseOr' (BinOp Or left right) rest' + parseOr' left rest = (left, rest) + +-- | Parse && +parseAnd :: [Token] -> (Expr, [Token]) +parseAnd toks = + let (left, rest) = parseComparison toks + in parseAnd' left rest + where + parseAnd' left (TkAnd : rest) = + let (right, rest') = parseComparison rest + in parseAnd' (BinOp And left right) rest' + parseAnd' left rest = (left, rest) + +-- | Parse comparison operators +parseComparison :: [Token] -> (Expr, [Token]) +parseComparison toks = + let (left, rest) = parseAddSub toks + in case rest of + (TkLt : rest') -> let (right, rest'') = parseAddSub rest' in (BinOp Lt left right, rest'') + (TkLe : rest') -> let (right, rest'') = parseAddSub rest' in (BinOp Le left right, rest'') + (TkGt : rest') -> let (right, rest'') = parseAddSub rest' in (BinOp Gt left right, rest'') + (TkGe : rest') -> let (right, rest'') = parseAddSub rest' in (BinOp Ge left right, rest'') + (TkEqEq : rest') -> let (right, rest'') = parseAddSub rest' in (BinOp Eq left right, rest'') + (TkNe : rest') -> let (right, rest'') = parseAddSub rest' in (BinOp Ne left right, rest'') + _ -> (left, rest) + +-- | Parse + and - +parseAddSub :: [Token] -> (Expr, [Token]) +parseAddSub toks = + let (left, rest) = parseMulDiv toks + in parseAddSub' left rest + where + parseAddSub' left (TkPlus : rest) = + let (right, rest') = parseMulDiv rest + in parseAddSub' (BinOp Add left right) rest' + parseAddSub' left (TkMinus : rest) = + let (right, rest') = parseMulDiv rest + in parseAddSub' (BinOp Sub left right) rest' + parseAddSub' left rest = (left, rest) + +-- | Parse * / % +parseMulDiv :: [Token] -> (Expr, [Token]) +parseMulDiv toks = + let (left, rest) = parseUnary toks + in parseMulDiv' left rest + where + parseMulDiv' left (TkStar : rest) = + let (right, rest') = parseUnary rest + in parseMulDiv' (BinOp Mul left right) rest' + parseMulDiv' left (TkSlash : rest) = + let (right, rest') = parseUnary rest + in parseMulDiv' (BinOp Div left right) rest' + parseMulDiv' left (TkPercent : rest) = + let (right, rest') = parseUnary rest + in parseMulDiv' (BinOp Mod left right) rest' + parseMulDiv' left rest = (left, rest) + +-- | Parse unary operators +parseUnary :: [Token] -> (Expr, [Token]) +parseUnary (TkMinus : rest) = + let (expr, rest') = parseUnary rest + in (UnaryOp Neg expr, rest') +parseUnary (TkNot : rest) = + let (expr, rest') = parseUnary rest + in (UnaryOp Not expr, rest') +parseUnary toks = parsePrimary toks + +-- | Parse primary expressions +parsePrimary :: [Token] -> (Expr, [Token]) +parsePrimary (TkNum n : rest) = (Lit n, rest) +parsePrimary (TkIdent name : TkLParen : rest) = + -- Function call + let (args, rest') = parseArgs rest + rest'' = expect TkRParen rest' + in (Call name args, rest'') +parsePrimary (TkIdent name : rest) = (Var name, rest) +parsePrimary (TkLParen : rest) = + let (expr, rest') = parseExpr rest + rest'' = expect TkRParen rest' + in (expr, rest'') +parsePrimary toks = error $ "Expected expression, got: " ++ show (take 3 toks) + +-- | Parse function arguments +parseArgs :: [Token] -> ([Expr], [Token]) +parseArgs (TkRParen : rest) = ([], TkRParen : rest) -- put back RParen +parseArgs toks = parseArgs' toks + where + parseArgs' ts = + let (expr, ts') = parseExpr ts + in case ts' of + (TkComma : ts'') -> + let (rest, ts''') = parseArgs' ts'' + in (expr : rest, ts''') + _ -> ([expr], ts') + +-- | Expect a specific token +expect :: Token -> [Token] -> [Token] +expect expected (tok : rest) + | tok == expected = rest + | otherwise = error $ "Expected " ++ show expected ++ ", got " ++ show tok +expect expected [] = error $ "Expected " ++ show expected ++ ", got EOF" + + + diff --git a/loopinv/examples/test1.c b/loopinv/examples/test1.c new file mode 100644 index 0000000..7d87183 --- /dev/null +++ b/loopinv/examples/test1.c @@ -0,0 +1,12 @@ +// Simple counting loop +// Expected: loop invariant 0 <= x <= n + +void simple(int n) { + int x = 0; + while (x < n) { + x = x + 1; + } +} + + + diff --git a/loopinv/examples/test2.c b/loopinv/examples/test2.c new file mode 100644 index 0000000..f5a0b32 --- /dev/null +++ b/loopinv/examples/test2.c @@ -0,0 +1,12 @@ +// Nested loop example +void nested(int n, int m) { + int i = 0; + while (i < n) { + int j = 0; + while (j < m) { + j = j + 1; + } + i = i + 1; + } +} + diff --git a/loopinv/examples/test3.c b/loopinv/examples/test3.c new file mode 100644 index 0000000..8fc0755 --- /dev/null +++ b/loopinv/examples/test3.c @@ -0,0 +1,8 @@ +// Countdown loop +void countdown(int n) { + int x = n; + while (x > 0) { + x = x - 1; + } +} + diff --git a/loopinv/examples/test_tricky.c b/loopinv/examples/test_tricky.c new file mode 100644 index 0000000..ff02a0c --- /dev/null +++ b/loopinv/examples/test_tricky.c @@ -0,0 +1,8 @@ +// Tricky loop - increment by 2 +void tricky(int n) { + int x = 0; + while (x < n) { + x = x + 2; + } +} +