From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: MIME-Version: 1.0 In-Reply-To: References: <149739530052.20686.9000645746376519779.stgit@dwillia2-desk3.amr.corp.intel.com> <149739530612.20686.14760671150202647861.stgit@dwillia2-desk3.amr.corp.intel.com> From: Dan Williams Date: Wed, 14 Jun 2017 10:02:36 -0700 Message-ID: Subject: Re: [PATCH v2 1/2] mm: improve readability of transparent_hugepage_enabled() To: Vlastimil Babka Cc: Andrew Morton , Jan Kara , "linux-nvdimm@lists.01.org" , Linux MM , linux-fsdevel , Ross Zwisler , Christoph Hellwig , "Kirill A. Shutemov" Content-Type: text/plain; charset="UTF-8" Sender: owner-linux-mm@kvack.org List-ID: On Wed, Jun 14, 2017 at 9:53 AM, Vlastimil Babka wrote: > On 06/14/2017 01:08 AM, Dan Williams wrote: >> Turn the macro into a static inline and rewrite the condition checks for >> better readability in preparation for adding another condition. >> >> Cc: Jan Kara >> Cc: Andrew Morton >> Reviewed-by: Ross Zwisler >> [ross: fix logic to make conversion equivalent] >> Acked-by: "Kirill A. Shutemov" >> Signed-off-by: Dan Williams > > Reviewed-by: Vlastimil Babka > > vbabka@gusiac:~/wrk/cbmc> cbmc test-thp.c > CBMC version 5.3 64-bit x86_64 linux > Parsing test-thp.c > file line 0: :0:0: warning: > "__STDC_VERSION__" redefined > file line 0: : note: this is the location of > the previous definition > Converting > Type-checking test-thp > file test-thp.c line 75 function main: function `assert' is not declared > Generating GOTO Program > Adding CPROVER library > Function Pointer Removal > Partial Inlining > Generic Property Instrumentation > Starting Bounded Model Checking > size of program expression: 171 steps > simple slicing removed 3 assignments > Generated 1 VCC(s), 1 remaining after simplification > Passing problem to propositional reduction > converting SSA > Running propositional reduction > Post-processing > Solving with MiniSAT 2.2.0 with simplifier > 4899 variables, 13228 clauses > SAT checker: negated claim is UNSATISFIABLE, i.e., holds > Runtime decision procedure: 0.008s > VERIFICATION SUCCESSFUL > > (and yeah, the v1 version fails :) Can you share the test-thp.c so I can add this to my test collection? I'm assuming cbmc is "Bounded Model Checker for C/C++"? -- To unsubscribe, send a message with 'unsubscribe linux-mm' in the body to majordomo@kvack.org. For more info on Linux MM, see: http://www.linux-mm.org/ . Don't email: email@kvack.org