Ticket #2252: BadPerform.2.hs

File BadPerform.2.hs, 1.3 KB (added by simona, 7 years ago)

simplifier output for BadPerform.hs

Line 
1-- Try running the convex hull algorithm.
2import Abs.Domain.SparsePolyhedra
3import Abs.Domain.SparsePolyhedra.Constraints
4import Abs.Domain.SparsePolyhedra.Types
5import Abs.Domain.SparsePolyhedra.Simplex
6import System.Environment (getArgs)
7import Data.List (sort)
8import Control.Monad (replicateM, replicateM_, liftM, unless) 
9
10-- Domain variables.
11
12-- | Size of the buffer
13s :: DomVar
14
15-- | The character read
16c :: DomVar
17
18-- | The NUL position
19sn :: DomVar
20
21-- | The pointer offset of u
22u :: DomVar
23
24-- | The NUL position of v
25vn :: DomVar
26
27-- | The NUL position of p
28tn :: DomVar
29
30-- | A flag determining if sn = 4 or 6
31f :: DomVar
32
33-- | The pointer offset of p
34p :: DomVar
35
36(s:c:sn:u:tn:p:f:vn:_) = [1..] :: [DomVar]
37
38main = do
39  let size = 8
40      initial = set u 0 $
41                top size
42  replicateM_ 1000 $ do
43    res1 <- fixpoint initial bottom bottom vn 1
44    unless (res1 `subset` res1) $ putStrLn "something's wrong"
45    res2 <- fixpoint initial bottom bottom vn 1
46    unless (res2 `subset` res2) $ putStrLn "something's wrong"
47
48
49fixpoint :: Poly -> Poly -> Poly -> DomVar -> Integer -> IO Poly
50fixpoint sU sT oldR sn fval = do
51  let sR = join sU sT
52  --putStrLn ("R:\n"++show sR)
53  let sV = meetAsym [Constraint (Terms [(1,u)]) 8] sR
54  if sR `subset` oldR then
55    return sV else do
56  let sT = assign 1 u (Constraint (Terms [(1,u)]) 1) sV
57  fixpoint sU sT sR sn fval
58